Contribution: Interface

Interface with PCoq environment.

Authors

Description

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)

Keywords

pcoq, graphical interface, environment, user interface

README

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).