aboutsummaryrefslogtreecommitdiffhomepage
path: root/CREDITS
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-19 20:13:59 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-19 20:13:59 +0000
commit8dd3376e5d7179b8185ba55be1e66b19e65deaec (patch)
tree9bcff0fd6b23c93a503f8e32cab45fba63535ec0 /CREDITS
parent7c51ef20064ed4f44a4e1dcb2040ec4b74919b5f (diff)
MAJ crédits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CREDITS')
-rw-r--r--CREDITS6
1 files changed, 6 insertions, 0 deletions
diff --git a/CREDITS b/CREDITS
index 6219ea8aa..b3d563caf 100644
--- a/CREDITS
+++ b/CREDITS
@@ -69,6 +69,11 @@ contrib/xml
developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
part of the ProofWeb project (Radbout University at Nijmegen, 2008)
+contrib/micromega
+ developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
+ extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
+ interface to the csdp solver uses code from John Harrison (University
+ of Cambridge, 1998)
parsing/search.ml
mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
theories/ZArith
@@ -115,6 +120,7 @@ of the Coq Proof assistant during the indicated time :
Hugo Herbelin (INRIA, 1996-now)
Gérard Huet (INRIA, 1985-1997)
Pierre Letouzey (LRI, 2000-2004 & PPS-Paris 7, 2005-now)
+ Evgeny Makarov (INRIA, 2007)
Pascal Manoury (INRIA, 1993)
Micaela Mayero (INRIA, 1997-2002)
Claude Marché (INRIA 2003-2004 & LRI, 2004-now)