From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- COPYRIGHT | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'COPYRIGHT') diff --git a/COPYRIGHT b/COPYRIGHT index 2cbb6fbc..7ed31f15 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -20,12 +20,6 @@ parsing/search.ml) Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier) Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml) -Coq includes a tactic Jp based on JProver, a theorem prover for -first-order intuitionistic logic. Jprover was originally implemented -by Stephan Schmitt and then integrated into MetaPRL by Aleksey -Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL -and then integrated it into Coq. - The file CREDITS contains a list of past contributors The credits section in Reference Manual introduction details contributions. @@ -38,4 +32,4 @@ The Coq development Team (march 2004) Pierre Letouzey (Université Paris Sud) Claude Marché (Université Paris Sud-INRIA) Christine Paulin (Université Paris Sud) - Clément Renard (INRIA) \ No newline at end of file + Clément Renard (INRIA) -- cgit v1.2.3