summaryrefslogtreecommitdiff
path: root/debian/copyright
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-02-01 21:58:59 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-02-01 21:58:59 +0000
commit3b182903454caa27cd34fc38c594970a800dc9a1 (patch)
tree0cb1e18612d495de06199f9d29ef4dd8764bc68e /debian/copyright
parent6b61b68d5822575015583047e1d266b8257e35d5 (diff)
Better handling of arch-indep packages.
Diffstat (limited to 'debian/copyright')
-rw-r--r--debian/copyright8
1 files changed, 4 insertions, 4 deletions
diff --git a/debian/copyright b/debian/copyright
index f4d56d47..c53b8733 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,14 +1,14 @@
This package was debianized by Fernando Sanchez <fer@debian.org>
-I was downloaded from
+It was downloaded from
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0pl1
+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-2004 The Coq development team,
+Copyright 1999-2005 The Coq development team,
INRIA-CNRS, University Paris Sud, All rights reserved.
This product includes also software developed by
@@ -17,7 +17,7 @@ This product includes also software developed by
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)
+ 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