From ad90c5f6a439d8e6981bf84178cdcd48483a3efc Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 21 Jul 2004 18:28:58 +0000 Subject: Getting ready for an upload to experimental. --- debian/copyright | 40 ++++++++++++++++++++++++++++++++++------ debian/patches/00list | 0 2 files changed, 34 insertions(+), 6 deletions(-) delete mode 100644 debian/patches/00list 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 -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 -- cgit v1.2.3