| Commit message (Expand) | Author | Age |
* | - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des | herbelin | 2008-05-10 |
* | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau | 2008-03-28 |
* | Petite modif pour pouvoir faire "intros until 0" qui introduit autant | aspiwack | 2008-02-29 |
* | Finish let| implementation and document it | msozeau | 2008-01-31 |
* | bug in accessing n-th abstraction | barras | 2008-01-18 |
* | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
* | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
* | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin | 2007-11-08 |
* | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin | 2007-09-21 |
* | 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-06-30 |
* | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin | 2007-05-29 |
* | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
* | Add functionality to permit printing terms with references to anonymous varia... | msozeau | 2007-02-16 |
* | correction d'un bug d'efficacite dans le printer | jforest | 2007-01-26 |
* | Évitement des noms de constructeurs dans les motifs de filtrage de "match" | herbelin | 2006-12-09 |
* | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
* | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin | 2006-05-19 |
* | - 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-27 |
* | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin | 2006-04-26 |
* | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
* | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
* | Version préliminaire d'inversion de la compilation du filtrage | herbelin | 2006-01-16 |
* | Standardisation du nom de subst_raw en subst_rawconstr | herbelin | 2006-01-11 |
* | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin | 2006-01-11 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Changement des named_context | gregoire | 2005-12-02 |
* | Types inductifs parametriques | mohring | 2005-11-02 |
* | Un vieux bug d'affichage des lieurs (cf bug #1005) | herbelin | 2005-09-06 |
* | Sur le conseil de X.Leroy: x=[||] devient Array.length x=0 | letouzey | 2005-08-19 |
* | HUGE COMMIT | sacerdot | 2005-01-03 |
* | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot | 2004-11-16 |
* | hiding the meta_map in evar_defs | barras | 2004-09-15 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ... | herbelin | 2004-07-11 |
* | Double bug d'affichage des cases dépendants (bug #784) | herbelin | 2004-06-28 |
* | Correction affichage v8 des records avec let (bug #798) | herbelin | 2004-06-27 |
* | Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ... | herbelin | 2004-03-28 |
* | bug de PP des fix (coqbugs #574) | barras | 2004-03-24 |
* | bug affichage des cofix | barras | 2004-03-09 |
* | correction de bugs des points fixes | barras | 2004-03-08 |
* | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras | 2004-03-05 |
* | Inclusion des annotations de type des filtrages dans 'Set Printing All' | herbelin | 2004-02-26 |
* | Relachement condition pour declarer un inductif dans la table des 'If'; contr... | herbelin | 2004-02-03 |
* | Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit... | herbelin | 2004-01-29 |
* | Substitution dans REvar; reparation bug 277 | herbelin | 2003-12-19 |
* | Changement de l'afficheur pour que les variables liées aient un nom indépen... | herbelin | 2003-09-23 |