The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

     Pcoq is a java-based graphical interface for Coq,
     (http://coq.inria.fr), in the family of CtCoq.  It runs under
     Unix and Microsoft Windows-(95, 98, NT).


     It is available from the web-page

             http://www-sop.inria.fr/lemme/pcoq


      Improvements with respect to CtCoq are:

      - More powerful mathematical notations are available,
      - It supports graphical illustration in Gif or jpeg,
      - It provides a debugger to help locate errors in compound
        tactics,
      - It is expected to run on all Unix architecture that support
        both ocaml and Java,
      - It is provided in binary form on Microsoft Windows,
      - It has a much simpler installation process, (rpm for redhat
        Linux, a simple graphical tool for Windows, sources with a
        simple make directive for other architectures).
      - The sources are freely available.


     Still, this is the very first release of this new piece of
     software and some useful functionalities from CtCoq have not
     been re-implemented in this new user-interface.  users are
     invited to send all comments and problem reports at the following
     address:

        
pcoq-request AT sophia.inria.fr


     Pcoq has been developed using Ocaml (http://caml.inria.fr),
     Aioli (http://www-sop.inria.fr/croap/aioli),
     Figue (http://www-sop.inria.fr/croap/figue), and
     Antlr (http://www.antlr.org).