| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-01-19 | Les records déclarés avec Record ne peuvent plus être récursifs (le | aspiwack |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-12-14 | Generalized binding syntax overhaul: only two new binders: `() and `{}, | msozeau |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | msozeau |
| 2008-11-05 | Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2007-04-25 | New keyword "Inline" for Parameters and Axioms for automatic | soubiran |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-09-01 | Suite commit 9110 (uniformisation position notation dans les blocs inductifs) | herbelin |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2006-01-11 | removes several warnings in contrib/interface | bertot |
| 2005-12-26 | Achèvement suppression traducteur dans contrib/interface | herbelin |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-03-03 | make sure the implicit argument indications are in the right order | bertot |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-10-23 | Conjecture declare maintenant un axiome; reorganisation VernacDefinition | herbelin |
| 2003-09-06 | Mise en place possibilité de définitions locales dans les paramètres des i... | herbelin |
| 2003-04-17 | Ajout "at next level" dans Notation | herbelin |
| 2003-04-09 | Réorganisation de Impargs + mise en place d'une infrastructure | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-02-05 | Ajout du traducteur | desmettr |
| 2003-01-22 | removes all references to ctast.ml the Makefile has been updated accordingly. | bertot |
| 2002-12-03 | la table PARAMETER n'existe plus (mergé dans la table CONSTANT) | letouzey |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-11-05 | Intégration des modifs de la branche mowgli : | herbelin |
| 2002-10-28 | Des critères plus fins d'analyse des implicites automatiques; meilleur affic... | herbelin |
| 2002-10-07 | Lazy manuelles dans le code | coq |
| 2002-10-06 | correcting the treatment of many tactics that use quant_hyp in file xlate.ml | bertot |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-07-11 | Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour | herbelin |
| 2002-06-03 | Intgration uniforme de coercions dans les dclarations (Variable and co) et re... | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2001-12-13 | compat ocaml 3.03 | filliatr |
| 2001-11-19 | Renommage qualid_of_global en shortest_qualid_of_global | herbelin |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-17 | Abstraction de l'immplementation de dirpath et implementation dans l'autre se... | herbelin |
| 2001-09-20 | Transparent | barras |
| 2001-08-10 | Prsing | herbelin |
| 2001-05-28 | Pretty -> Prettyp | filliatr |
| 2001-04-04 | Files that handle the dialogue with the graphical user-interface pcoq. | bertot |
