diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-21 18:28:58 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-21 18:28:58 +0000 |
| commit | ad90c5f6a439d8e6981bf84178cdcd48483a3efc (patch) | |
| tree | 86445e1b02d87a2047108f2240b47509aefa0507 /debian | |
| parent | 21aeec569d7b4d1feb3e4984e2f1138bd30f1625 (diff) | |
Getting ready for an upload to experimental.
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/copyright | 40 | ||||
| -rw-r--r-- | debian/patches/00list | 0 |
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 |