| Age | Commit message (Expand) | Author |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-08-07 | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-07-15 | - Granted wish #2138 (support for local binders in syntax of Record fields). | herbelin |
| 2009-06-03 | Ensure the precondition of the partial function [list_chop] holds | msozeau |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-11-23 | Fixed bug #2006 (type constraint on Record was not taken into account) + | herbelin |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-07-25 | Correction d'une incohérence de typage des inductifs polymorphes: les | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-05-22 | Strategy commands are now exported | barras |
| 2008-05-21 | refined the conversion oracle | barras |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-15 | - Add "Global" modifier for instances inside sections with the usual | msozeau |
| 2008-04-12 | Document the new setoid rewrite tactic, and fix a few things while | msozeau |
| 2008-03-30 | Ajout d'abbréviations/notations paramétriques | herbelin |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-02-19 | added products and sorts as possible heads for canonical structures | corbinea |
| 2008-02-14 | Added default canonical structures (see example in test-suite) | corbinea |
| 2008-02-01 | Beaoucoup de changements dans la representation interne des modules. | soubiran |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-14 | Correction ordre d'affichage des champs des Record | herbelin |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-10-05 | Correction de quelques défauts d'affichage (notations sous "as" pour | herbelin |
| 2007-05-28 | Réaffichage des Structure/Record sous la forme Record | herbelin |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2006-12-08 | Suite ajout option -output-context | herbelin |
| 2006-12-08 | Ajout d'une option -output-context qui affiche le contexte en CCI pur à la | herbelin |
| 2006-10-29 | Compatibilité du polymorphisme de constantes avec les sections. | herbelin |
| 2006-10-28 | Ajout option Set Printing Universes et amélioration affichage des univers | herbelin |
| 2006-09-23 | Déplacement surround dans util.ml et parenthésage des déclarations | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-01-28 | Correction bug Inspect introduit par le passage du discharge à une méthode ... | 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 (mécanis... | herbelin |
| 2005-11-21 | Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05) | herbelin |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-08-19 | pas besoin de List.length pour savoir si une liste est vide | letouzey |
| 2005-02-20 | Keep ClosedSection marker for reset | herbelin |
| 2005-02-18 | Renaming Print Canonical Structure into Print Canonical Projections | herbelin |