| Age | Commit message (Expand) | Author |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2008-10-15 | Report des commits 11417 et 11437 de la v8.2 | soubiran |
| 2008-06-25 | Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio... | notin |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-04-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2007-02-21 | Fixed the pseudo-cicularity problem due to the with operator on Module Type. | soubiran |
| 2007-01-24 | modifications des messages d'erreurs renvoyés lors de la comparaison | soubiran |
| 2006-05-23 | Modification de add_glob (support des modules dans Coqdoc) | notin |
| 2005-02-18 | Moved Indmap and ConstrMap from Libnames to Names for use in Cooking | herbelin |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 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-07-16 | Nouvelle en-tête | herbelin |
| 2003-01-22 | id_of_msid en plus | letouzey |
| 2002-12-09 | Corrections de gestion des univers et modules + meilleure gestions des noms... | coq |
| 2002-12-05 | des Set et des Map en plus | letouzey |
| 2002-12-04 | Corrige un bug de composition de substitutions | coq |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-19 | Pretty-printing preliminaire des modules, commandes | coq |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2001-11-29 | reparation de Locate | barras |
| 2001-11-29 | nouvel algo de conversion plus uniforme | barras |
| 2001-11-12 | Suites modifs du noyau. Univ devient purement fonctionnel. | barras |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-17 | Abstraction de l'immplementation de dirpath et implementation dans l'autre se... | herbelin |
| 2001-10-12 | Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra... | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-09-20 | Transparent | barras |
| 2001-09-20 | Compatibilté make doc | herbelin |
| 2001-08-10 | Parsing | herbelin |
| 2001-08-01 | Ajout add_prefix/add_suffix | herbelin |
| 2001-03-15 | entetes | filliatr |
| 2001-03-01 | Déplacement de qualid dans Nametab, hors du noyau | herbelin |
| 2001-02-16 | ident au lieu de string pour le nom de base de qualid | herbelin |
| 2001-02-14 | Mise en place d'un système optionnel de discharge immédiat; prise en compte... | herbelin |
| 2001-01-27 | Ajout alias mutual_inductive_path = section_path | herbelin |
| 2000-12-25 | Alias variable_path | herbelin |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-12-05 | Mini-nettoyage noms longs | herbelin |
| 2000-11-29 | Ajout d'un test pour vérifier qu'on a affaire à un ident | herbelin |
| 2000-11-26 | Prise en compte de noms absolus dans la nametab | herbelin |
| 2000-11-23 | Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp | herbelin |
| 2000-11-22 | Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's... | herbelin |
| 2000-11-21 | implicites manuels | filliatr |
| 2000-11-20 | Introduction constant_path = section_path | herbelin |
| 2000-11-07 | Nettoyage Names suite | herbelin |
| 2000-11-06 | Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ... | herbelin |