| Age | Commit message (Expand) | Author |
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-14 | Makefile: ml dependencies of contribs are moved to .mllib files | letouzey |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2009-01-14 | Fixing #1960 (xml bug with external on goal variable) and #1961 | herbelin |
| 2008-12-19 | Nettoyage des variables Coq et amélioration de coqmktop. Les | notin |
| 2008-11-27 | fixed non-exhaustive pattern matching | barras |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-21 | Addded the "Dump Tree" command. | cek |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2007-06-21 | Correction de plusieurs bugs de l'export XML (utilisation d'un type de | herbelin |
| 2007-01-22 | Correction du bug #1315: | notin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-10-16 | affichage des ... dans les scripts | barras |
| 2006-10-03 | Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ... | herbelin |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-07-18 | Correction bug #1192 | notin |
| 2006-07-07 | Correction bug 1172 + correction en passant de la taille des paramètres de f... | herbelin |
| 2006-05-23 | Clarification role de library_part : renommage en remove_section_part | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-04-28 | Standardisation du nom des méthodes de Evd | herbelin |
| 2006-04-27 | Message d'erreur plus informatif | herbelin |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-01 | Correction bug #842 (rename d'une hyp du contexte) | herbelin |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-26 | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-08-19 | pas besoin de List.length pour savoir si une liste est vide | letouzey |
| 2005-05-20 | Adoption du nom canonique global_of_constr pour éviter confusion avec type r... | herbelin |
| 2005-03-15 | Unsharing before exportation to ensure uniqueness of xml id's | herbelin |
| 2005-02-18 | Standardisation of function names about structures | herbelin |
| 2005-02-04 | Ajout printer direct cic vers xml | herbelin |
| 2005-02-04 | Export du printer xml vers tacinterp | herbelin |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2005-01-02 | Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan... | herbelin |
| 2004-12-03 | Orthographe! | herbelin |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-10-11 | Suppression IsConjecture redondant avec Conjectural | herbelin |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-08 | The innersort is now computed as the more precise sort between the | sacerdot |