From b7e4eb4bf5b05b69bb4b2e1c467871acd931fc1e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Jan 2009 20:10:55 +0000
Subject: - Standardized prefix use of "Local"/"Global" modifiers as decided in
   late 2008 Coq WG. - Updated Copyright file wrt JProver.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 COPYRIGHT | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'COPYRIGHT')

diff --git a/COPYRIGHT b/COPYRIGHT
index 2cbb6fbce8..7ed31f15d7 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