aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Change syntax of Hint Resolve to actually accept user-given priorities.Gravatar msozeau2013-09-07
* * parsing/Lexer: Cosmetics.Gravatar regisgia2013-09-02
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
* Granting bug #3098: adding priority to Existing Instances.Gravatar ppedrot2013-08-01
* More dynamic argument scopesGravatar letouzey2013-07-17
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Reorganizing intropatterns: * and ** are not naming intropatterns.Gravatar herbelin2013-07-09
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Removed the ad-hod handling of wit_tacticn.Gravatar ppedrot2013-07-02
* Fixing Camlp4 compilation.Gravatar ppedrot2013-06-30
* Added a generic handler of Ltac quotations, based on the existingGravatar ppedrot2013-06-27
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Revert "KEYID token makes parsing more robust in face of notations"Gravatar gareuselesinge2013-06-21
* Revert "parse "of" as KEYID "of""Gravatar gareuselesinge2013-06-21
* parse "of" as KEYID "of"Gravatar gareuselesinge2013-06-19
* KEYID token makes parsing more robust in face of notationsGravatar gareuselesinge2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* More comments in Genarg.Gravatar ppedrot2013-06-06
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Setting "appcontext" as the default behaviour in Ltac matching.Gravatar ppedrot2013-05-28
* Fixing warning of deprecated Argument Scopes.Gravatar ppedrot2013-05-28
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Egramcoq+Lexer : no need for an init_functionGravatar letouzey2013-04-23
* Egramcoq: clean an ugly code snippetGravatar letouzey2013-04-23
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* More functional implementation of locality_flag and program_modeGravatar gareuselesinge2013-04-15
* cbn can be called by EvalGravatar pboutill2013-03-25
* Pptactic.pr_raw_tactic is now without env argumentGravatar letouzey2013-03-14
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13