From 3a8946b8b1a77941f02e80230286280ee86d23a0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 22 Mar 2009 22:01:32 +0000 Subject: Backport from v8.2 branch of 11986 (interpretation of quantified hypotheses in induction, unbalanced parenthesis in ltac call stack printer) and 12003 (late update of CREDITS) + update of magic numbers (using a somehow arbitrary value between the 8.2 magic numbers and the possibly forthcoming 8.3 magic numbers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12007 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index c982d6724..3587eec59 100644 --- a/CREDITS +++ b/CREDITS @@ -50,8 +50,6 @@ plugins/interface at Nijmegen, 2007-2008) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) -plugins/recdef - developed by Yves Bertot (INRIA-Marelle, 2005-2006) plugins/ring developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick Loiseleur (LRI, 1997-1999) @@ -80,16 +78,21 @@ theories/ZArith started by Pierre Crégut (France Telecom R&D, 1996) theories/IntMap developed by Jean Goubault-Larrecq (Dyade, 1998) +theories/Numbers/Cyclic + developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry + (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and + Pierre Letouzey (PPS-Paris 7, 2008) theories/Strings developed by Laurent Théry (INRIA-Lemme, 2003) ide/utils some files come from Maxence Guesdon's Cameleon tool -Many discussions within the Démons team at LRI and the LogiCal project -influenced significantly the design of Coq especially with +Many discussions within the Démons team at LRI, and the +LogiCal/TypiCal projects influenced significantly the design of +components of Coq, especially with - J. Courant, P. Courtieu, J. Duprat, J. Goubault, - A. Miquel, C. Marché, B. Monate, B. Werner. + F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault, + A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner. Intensive users suggested improvements of the system : @@ -135,9 +138,11 @@ of the Coq Proof assistant during the indicated time : LRI, 1997-now) Clément Renard (INRIA, 2001-2004) Claudio Sacerdoti Coen (INRIA, 2004-2005) + Amokrane Saïbi (INRIA, 1993-1998) + Vincent Siles (INRIA, 2007) + Élie Soubiran (INRIA, 2007-now) Matthieu Sozeau (INRIA, 2005-now) Arnaud Spiwack (INRIA, 2006-now) - Amokrane Saïbi (INRIA, 1993-1998) Benjamin Werner (INRIA, 1989-1994) *************************************************************************** -- cgit v1.2.3