aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_constr.ml4
Commit message (Expand)AuthorAge
...
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Diverses corrections Gravatar herbelin2008-04-14
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* - Correction bug dans syntaxe des match (liste de motifs vide était acceptée)Gravatar herbelin2007-08-22
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Prise en compte réversibilité des notations de la forme "Notation Nil := @n...Gravatar herbelin2007-05-10
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11
* Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5Gravatar herbelin2007-04-10
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.Gravatar msozeau2007-02-16
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Abbreviation of order notation.Gravatar msozeau2007-02-01
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
* Notations:Gravatar herbelin2006-10-09
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Correction incohérence parsing de %delim dans les motifsGravatar herbelin2006-07-12
* Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...Gravatar herbelin2006-07-04
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-19 06:29:09 +0000