Interface with PCoq environment.
- Yves Bertot
Pcoq provides a working environment for the Coq theorem prover (it includes extra contributions from Loïc Pottier and Laurence Rideau, INRIA Lemme-Marelle, and an extension by Lionel Mamane, Radboud university, Nijmegen, as part of the TeXMacs project)
pcoq, graphical interface, environment, user interface
Interface plugin ================ This contribution was previously maintained as part of the official distribution. It provides custom toplevels that might be useful for graphical interfaces. Main Makefile targets: all check opt byte install The coq-interface and coq-parser binaries are not built; they can be simulated using dynamic loading (see how tests are made in the Makefile).