| Age | Commit message (Expand) | Author |
|---|
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-05-26 | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin |
| 2008-05-12 | - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to | msozeau |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-05-06 | Better parsing of typeclasses, any constr is allowed for ! bindings so | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-04-26 | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin |
| 2008-04-14 | Diverses corrections | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 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 |
