diff options
Diffstat (limited to 'debian/copyright')
| -rw-r--r-- | debian/copyright | 76 |
1 files changed, 29 insertions, 47 deletions
diff --git a/debian/copyright b/debian/copyright index 38373808..6ff2511f 100644 --- a/debian/copyright +++ b/debian/copyright @@ -1,47 +1,29 @@ -This package was debianized by Fernando Sanchez <fer@debian.org> - -It was downloaded from - -ftp://ftp.inria.fr/INRIA/LogiCal/coq/current - -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-2005 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 - -Copyright: the Coq Proof Assistant is distributed under the terms of the GNU -Lesser General Public Licence, version 2.1, see -/usr/share/common-licenses/LGPL-2.1. - -However there are two exceptions: files in the directories contrib/jprover and -ide/utils are distributed under the terms of the GNU General Public Licence, -see /usr/share/common-licenses/GPL-2. +Packaged-By: Fernando Sanchez <fer@debian.org> +Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 +Original-Source-Location: http://coq.inria.fr/ + +Files: * +Copyright: © 1999-2010 The Coq development team, + INRIA, CNRS, University Paris Sud, + University Paris 7, Ecole Polytechnique. +License: LGPL-2.1 + + This product includes also software developed by + 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 /usr/share/doc/coq/CREDITS.gz contains a list of contributors. + + The Coq Proof Assistant is distributed under the terms of the GNU + Lesser General Public Licence, version 2.1, see + /usr/share/common-licenses/LGPL-2.1. + +Files: debian/* +Copyright: © 1999-2000 Fernando Sanchez <fer@debian.org> + © 2001-2002 Judicael Courant <Judicael.Courant@lri.fr> + © 2004-2009 Samuel Mimram <smimram@debian.org> + © 2008-2010 Stéphane Glondu <glondu@debian.org> +License: LGPL-2.1 |