From 253ba3b3b5d4066bd0af4ba9588311c2bb0bbd06 Mon Sep 17 00:00:00 2001 From: Pav Lucistnik Date: Sat, 16 Oct 2004 00:55:32 +0000 Subject: 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 --- math/Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'math/Makefile') diff --git a/math/Makefile b/math/Makefile index 9d64e6438405..78dafd9e0caa 100644 --- a/math/Makefile +++ b/math/Makefile @@ -28,6 +28,7 @@ SUBDIR += cln SUBDIR += concorde SUBDIR += convertall + SUBDIR += coq SUBDIR += cxsc SUBDIR += dcdflib SUBDIR += diehard -- cgit v1.2.3