Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

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)