This editor is used to edit interactive theorem prover files within
It is made to use with Coq,
and in a near future PVS and other
It uses a lightweight approach: easy to extend,
with just a minimal set of commands.
For more technical informations about it, see the
1 Installation and requirements
2 Basic Configurations
These configurations are mandatory if you want Prover Editor to work.
3 Some uses
ProverEditor will be part of the Mobius
This documentation is maintained since the first birthday of
was once CoqEditor for Eclipse, september the 25th 2006, and it was
generated on the 27th September, 2006.
This document was translated from LATEX by