| Age | Commit message (Expand) | Author |
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-12-01 | Continuing r12485-12486 (cleaning around name generation) | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Took local definitions into account in the test for deciding whether | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-02 | Improved parameterization of Coq: | herbelin |
| 2009-03-28 | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau |
| 2008-11-05 | Move Record desugaring to constrintern and add ability to use notations | msozeau |
| 2008-10-23 | Open notation for declaring record instances. | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-08 | - Patch sur "intros until 0" | herbelin |
| 2008-05-10 | - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-02-29 | Petite modif pour pouvoir faire "intros until 0" qui introduit autant | aspiwack |
| 2008-01-31 | Finish let| implementation and document it | msozeau |
| 2008-01-18 | bug in accessing n-th abstraction | barras |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 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-11-08 | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin |
| 2007-09-21 | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin |
| 2007-06-30 | Correction bug sur factorisation affichage paramètres (cf r9918) | herbelin |
| 2007-06-30 | Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record | herbelin |
| 2007-05-29 | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-02-16 | Add functionality to permit printing terms with references to anonymous varia... | msozeau |
| 2007-01-26 | correction d'un bug d'efficacite dans le printer | jforest |
| 2006-12-09 | Évitement des noms de constructeurs dans les motifs de filtrage de "match" | herbelin |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-05-19 | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-26 | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-01-16 | Version préliminaire d'inversion de la compilation du filtrage | herbelin |
| 2006-01-11 | Standardisation du nom de subst_raw en subst_rawconstr | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-09-06 | Un vieux bug d'affichage des lieurs (cf bug #1005) | herbelin |
| 2005-08-19 | Sur le conseil de X.Leroy: x=[||] devient Array.length x=0 | letouzey |
| 2005-01-03 | HUGE COMMIT | sacerdot |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |