summaryrefslogtreecommitdiff
path: root/COPYRIGHT
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
commitb9f47391f7f259c24119d1de0a87839e2cc5e80c (patch)
tree26dd3d5de63f420384fd84196d3a144af01f6084 /COPYRIGHT
parent5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (diff)
Imported Upstream snapshot 8.3~beta0+13323
Diffstat (limited to 'COPYRIGHT')
-rw-r--r--COPYRIGHT43
1 files changed, 11 insertions, 32 deletions
diff --git a/COPYRIGHT b/COPYRIGHT
index 63d90573..8d81d8c4 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,35 +1,14 @@
-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.
+ The Coq proof assistant
-Copyright 1999-2004 The Coq development team,
-INRIA-CNRS, University Paris Sud, All rights reserved.
-
-This version contains modifications by Lionel Elie Mamane
-<lionel@mamane.lu> done while under employment of the Radboud
-University Nijmegen. However, no copyright-assignment-to-employer
-agreement was signed, and copyright of articles and books written on
-work time rest with the employee. By analogy, it is Lionel's opinion
-that copyright on these changes rests with him.
+Copyright 1999-2010 The Coq development team, INRIA, CNRS, University
+Paris Sud, University Paris 7, Ecole Polytechnique.
This product includes also software developed by
- Yves Bertot, Lemme, INRIA Sophia-Antipolis (plugins/interface,
-parsing/search.ml)
- Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
- Pierre Courtieu, Lemme (plugins/funind)
- Loïc Pottier, Lemme, INRIA Sophia-Antipolis (plugins/fourier)
- Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
-
-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)
+ Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
+ Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
+ Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
+ Pierre Corbineau, Radbout University, Nijmegen (declarative mode)
+ John Harrison, University of Cambridge (csdp wrapper)
+
+The file CREDITS contains a list of contributors.
+The credits section in the Reference Manual details contributions.