From 2d9b791f57018904acd0d7c154f486c40bbffca0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 16 Jul 2010 18:26:32 +0200 Subject: Refresh copyright file --- debian/copyright | 94 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/debian/copyright b/debian/copyright index 38373808..450d3086 100644 --- a/debian/copyright +++ b/debian/copyright @@ -1,47 +1,47 @@ -This package was debianized by Fernando Sanchez - -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 +Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 +Original-Source-Location: http://coq.inria.fr/ + +Files: * +Copyright: © 1999-2004 The Coq development team, + INRIA-CNRS, University Paris Sud +License: LGPL-2.1 + + 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 version contains modifications by Lionel Elie Mamane + 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. + + 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 /usr/share/doc/coq/CREDITS.gz contains a list of + developpers and contributors. + + 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 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. -- cgit v1.2.3