summaryrefslogtreecommitdiff
path: root/CREDITS
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /CREDITS
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'CREDITS')
-rw-r--r--CREDITS15
1 files changed, 9 insertions, 6 deletions
diff --git a/CREDITS b/CREDITS
index eba2a4a4..2e61259f 100644
--- a/CREDITS
+++ b/CREDITS
@@ -38,15 +38,16 @@ contrib/first-order
contrib/fourier
developed by Loïc Pottier (INRIA-Lemme, 2001)
contrib/funind
- developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2006)
- and Julien Forest, Benjamin Grégoire and Gilles Barthe (INRIA-Everest, 2006)
+ developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2006),
+ Julien Forest (INRIA-Everest, 2006)
+ and Yves Bertot (INRIA-Marelle, 2005-2006).
contrib/interface
developed by Yves Bertot with contributions from Loïc Pottier and
Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006)
contrib/omega
developed by Pierre Crégut (France Telecom R&D, 1996)
contrib/recdef
- developed by Yves Bertot (INRIA-Marelle, 2005)
+ developed by Yves Bertot (INRIA-Marelle, 2005-2006)
contrib/ring
developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
Loiseleur (LRI, 1997-1999)
@@ -55,8 +56,9 @@ contrib/romega
contrib/rtauto
developed by Pierre Corbineau (LRI, 2005)
contrib/setoid_ring
- developed by Benjamin Grégoire, Assia Mahboubi (INRIA-Marelle, 2005-2006)
- and Bruno Barras (INRIA LogiCal, 2005-2006)
+ developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
+ Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
+ and Bruno Barras (INRIA LogiCal, 2005-2006),
contrib/subtac
developed by Matthieu Sozeau (LRI, 2005-2006)
contrib/xml
@@ -85,7 +87,7 @@ Intensive users suggested improvements of the system :
Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme projects),
C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
P. Castéran (University Bordeaux 1),
- The Foundations Group (Radboub University, Nijmegen, The Netherlands),
+ The Foundations Group (Radboud University, Nijmegen, The Netherlands),
Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis).
The following people have contributed to the development of different versions
@@ -94,6 +96,7 @@ of the Coq Proof assistant during the indicated time :
Bruno Barras (INRIA, 1995-now)
Jacek Chrzaszcz (LRI, 1998-2003)
Thierry Coquand (INRIA, 1985-1989)
+ Pierre Corbineau (LRI, 2003-now)
Cristina Cornes (INRIA, 1993-1996)
Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
David Delahaye (INRIA, 1997-2002)