Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 34 insertions, 0 deletions

diff --git a/COPYRIGHT b/COPYRIGHT
new file mode 100644
index 00000000..ac7d87df
--- /dev/null
+++ b/COPYRIGHT
@@ -0,0 +1,34 @@
+The Coq proof assistant V7 and V8 includes software developed by the 
+Coq development team inside the LogiCal project, at INRIA, CNRS and
+University Paris Sud. 
+
+Copyright 1999-2004 The Coq development team, 
+INRIA-CNRS, University Paris Sud, All rights reserved.
+
+This product includes also software developed by
+	Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
+parsing/search.ml)
+	Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
+	Pierre Courtieu, Lemme (contrib/funind)
+	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.
+
+The Coq development Team (march 2004)
+	Bruno Barras (INRIA)
+	Pierre Corbineau (Université Paris Sud)
+	Jean-Christophe Filliâtre (CNRS)
+	Hugo Herbelin (INRIA)
+	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