summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-21 18:28:58 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-21 18:28:58 +0000
commitad90c5f6a439d8e6981bf84178cdcd48483a3efc (patch)
tree86445e1b02d87a2047108f2240b47509aefa0507 /debian
parent21aeec569d7b4d1feb3e4984e2f1138bd30f1625 (diff)
Getting ready for an upload to experimental.
Diffstat (limited to 'debian')
-rw-r--r--debian/copyright40
-rw-r--r--debian/patches/00list0
2 files changed, 34 insertions, 6 deletions
diff --git a/debian/copyright b/debian/copyright
index 59529f30..f4d56d47 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,11 +1,39 @@
This package was debianized by Fernando Sanchez <fer@debian.org>
-The "Coq proof assistant" was developed conjointly by
- INRIA (since 1985),
- Laboratoire de l'Informatique du Parallelisme LIP
- associated to CNRS and ENS Lyon (sept.89-sept.97),
- Laboratoire de Recherche en Informatique
- associated to CNRS and Paris 11 (since sept. 97).
+I was downloaded from
+
+ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0pl1
+
+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 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)
The complete list of developpers and contributors can be found in
/usr/share/doc/doc/CREDITS.gz
diff --git a/debian/patches/00list b/debian/patches/00list
deleted file mode 100644
index e69de29b..00000000
--- a/debian/patches/00list
+++ /dev/null