The Coq mailing list

[Laurent Thery <Laurent.Thery AT sophia.inria.fr>]

Hi,

We are happy to announce the first official release of Cyp.

Cyp is a tool that proposes a generic solution to bridge the gap between 
the usual paper and pencil proof and its corresponding tactic-based formal
script.


Information on Cyp are available at:

ftp://ftp-sop.inria.fr/lemme/cyp/index.html

To run cyp, for coq 8.0 do

java -jar cyp.jar -p coq


for coq 7.4, do

java -jar cyp.jar -p coq7


--
Laurent Théry