aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
Commit message (Expand)AuthorAge
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Misc fixes.Gravatar msozeau2009-11-06
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Module type expressions of the form (Fsig X) with Definition foo := bar are n...Gravatar soubiran2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
* 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
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Do not reserve the keyword "Infer".Gravatar puech2009-02-03
* 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
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* - 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
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* 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
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - 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
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* 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
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Strategy commands are now exportedGravatar barras2008-05-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 10:49:26 +0000