summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/copyright16
1 files changed, 8 insertions, 8 deletions
diff --git a/debian/copyright b/debian/copyright
index c53b8733..f0856000 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -14,9 +14,9 @@ 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 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)
+ 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
@@ -27,13 +27,13 @@ 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)
+ 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)
+ 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