aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* Oops... forgot to commit a file related to r11561.Gravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalGravatar herbelin2008-06-06
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* - 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
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* 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
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-12 09:27:06 +0000