aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...Gravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* 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
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Misc fixes.Gravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* 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
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
* fixed bug in Czar grammarGravatar corbinea2009-10-25
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Complement to 12347 and 12348 on the extended syntax of case/elim.Gravatar herbelin2009-09-27
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
* 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
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* 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
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
* Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansGravatar aspiwack2009-05-27
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...Gravatar aspiwack2009-05-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 08:40:22 +0000