summaryrefslogtreecommitdiff
path: root/COPYRIGHT
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /COPYRIGHT
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'COPYRIGHT')
-rw-r--r--COPYRIGHT8
1 files changed, 1 insertions, 7 deletions
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)