K 10 svn:author V 3 pav K 8 svn:date V 27 2004-10-16T00:55:32.000000Z K 7 svn:log V 429 Add coq, a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification "kernel". PR: ports/72718 Submitted by: Rene Ladan END