| Age | Commit message (Expand) | Author |
|---|
| 2009-11-27 | Added support for definition of fixpoints using tactics. | herbelin |
| 2009-11-04 | Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names. | gmelquio |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2009-03-29 | Avoid inadvertent declaration of "on" as a keyword. New syntax is | msozeau |
| 2009-03-28 | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau |
| 2008-12-14 | Generalized binding syntax overhaul: only two new binders: `() and `{}, | msozeau |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | 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-10-23 | Generalized implementation of generalization. | msozeau |
| 2008-10-22 | A much better implementation of implicit generalization: | msozeau |
| 2008-10-22 | Affichage des notations récursives: | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-07-07 | - Improve [Context] vernacular to allow arbitrary binders, not just | msozeau |
| 2008-07-04 | Fixes in handling of implicit arguments: | msozeau |
| 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 |
