From c0d7196603f1ca4ff5f30b39cf67be75f1a1f26c Mon Sep 17 00:00:00 2001
From: mohring
Date: Mon, 15 Mar 2004 14:31:58 +0000
Subject: Ajout d'un fichier COPYRIGHT

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5491 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 COPYRIGHT | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 COPYRIGHT

diff --git a/COPYRIGHT b/COPYRIGHT
new file mode 100644
index 0000000000..ac7d87dfa2
--- /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
-- 
cgit v1.2.3