aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-07Change syntax of Hint Resolve to actually accept user-given priorities.msozeau
2013-09-02* parsing/Lexer: Cosmetics.regisgia
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08Support Proof Generalgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-01Added a Print Debug GC command that displays the current state ofppedrot
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-07-09Reorganizing intropatterns: * and ** are not naming intropatterns.herbelin
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-07-02Removed the ad-hod handling of wit_tacticn.ppedrot
2013-06-30Fixing Camlp4 compilation.ppedrot
2013-06-27Added a generic handler of Ltac quotations, based on the existingppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-27Removing useless tactic arguments, and using generic argumentsppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-21Revert "KEYID token makes parsing more robust in face of notations"gareuselesinge
2013-06-21Revert "parse "of" as KEYID "of""gareuselesinge
2013-06-19parse "of" as KEYID "of"gareuselesinge
2013-06-19KEYID token makes parsing more robust in face of notationsgareuselesinge
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-06More comments in Genarg.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
2013-05-28Fixing warning of deprecated Argument Scopes.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-23Egramcoq+Lexer : no need for an init_functionletouzey
2013-04-23Egramcoq: clean an ugly code snippetletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-25cbn can be called by Evalpboutill
2013-03-14Pptactic.pr_raw_tactic is now without env argumentletouzey
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
2013-02-19Dir_path --> DirPathletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 10:10:32 +0000