| Age | Commit message (Expand) | Author |
| 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 |
| 2004-07-11 | Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ... | herbelin |
| 2004-06-28 | Double bug d'affichage des cases dépendants (bug #784) | herbelin |
| 2004-06-27 | Correction affichage v8 des records avec let (bug #798) | herbelin |
| 2004-03-28 | Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ... | herbelin |
| 2004-03-24 | bug de PP des fix (coqbugs #574) | barras |
| 2004-03-09 | bug affichage des cofix | barras |
| 2004-03-08 | correction de bugs des points fixes | barras |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-02-26 | Inclusion des annotations de type des filtrages dans 'Set Printing All' | herbelin |
| 2004-02-03 | Relachement condition pour declarer un inductif dans la table des 'If'; contr... | herbelin |
| 2004-01-29 | Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit... | herbelin |