---

1

GeoProof is dynamic geometry software which can be used in conjunction with CoqIDE to interactively build a Coq statement corresponding to a geometric figure. More information about GeoProof can be found here: http://home.gna.org/geoproof/