CtCoq

The CtCoq system: Design and architecture. CtCoq provides a working environment for the Coq theorem prover. It has been developed following a general approach for building user-interfaces for theorem provers. It has the following characteristics: ... Ctcoq is now replaced by a new system, called pcoq