| Age | Commit message (Expand) | Author |
|---|
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2008-01-15 | Generalize instance declarations to any context, better name handling. Add ho... | msozeau |
| 2008-01-07 | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau |
| 2008-01-05 | Correction bug #1749 (datant de l'implantation des or-patterns) + | 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-09-28 | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu |
| 2007-08-22 | - Correction bug dans syntaxe des match (liste de motifs vide était acceptée) | herbelin |
| 2007-07-16 | Generalized CAMLP4USE for pp dependencies | corbinea |
| 2007-07-11 | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey |
| 2007-05-10 | Prise en compte réversibilité des notations de la forme "Notation Nil := @n... | herbelin |
| 2007-04-11 | Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a | herbelin |
| 2007-04-10 | Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5 | herbelin |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-02-16 | Add 'dest obj as pat in body' keyword as a pattern-matching shortcut. | msozeau |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-02-01 | Abbreviation of order notation. | msozeau |
| 2007-01-31 | Fix order of wf and measure arguments, patch Program doc. | msozeau |
| 2006-12-03 | Remplacement de la dépendance de G_vernac en G_constr (source | herbelin |
| 2006-10-09 | Notations: | herbelin |
| 2006-07-22 | - Ajout d'un cast vm dans la syntaxe : x <: t | bgregoir |
| 2006-07-12 | Correction incohérence parsing de %delim dans les motifs | herbelin |
| 2006-07-04 | Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ... | herbelin |
| 2006-07-03 | Extension des motifs disjonctifs au cas de disjonction de motifs multiples | herbelin |
| 2006-06-22 | Added {measure x f} as a valid recursion order. | msozeau |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-04-27 | Standardisation nom option_app en option_map | 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 |
| 2005-12-30 | Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de... | herbelin |
| 2005-12-26 | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2004-12-24 | Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque... | herbelin |
| 2004-11-17 | Déclaration de '..' comme mot-clé (résoud bug #856) | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-17 | Parsing des V8Notation avec motif recursif en v7 | herbelin |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-02-26 | Keep structure information for Fixpoint declaration and Fix terms | bertot |
| 2003-11-14 | Compatibilite %T | herbelin |
| 2003-11-03 | Compatibilite V7.4 pour le delimiteur de positive | herbelin |
| 2003-10-10 | Delimiters N devient 'nat' | herbelin |
| 2003-09-22 | traducteur: affiche les commentaires a l'interieur des commandes | barras |
| 2003-09-21 | Mise en place d'implicites par noms en v8 | herbelin |
| 2003-09-12 | Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c... | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-06-11 | Token '.(' seulement pour v8, sinon conflit avec '.(*' | herbelin |
| 2003-06-10 | Ajout notation c.(f) en v8 pour les projections de Record | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-03-27 | Affinement nommage des productions | herbelin |
