aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-22Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.herbelin
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-04Early translation of camlp4/camlp5 located errors into coq-locatedherbelin
2012-11-25Monomorphization (parsing)ppedrot
2012-11-15backtrack too much commited files in the last commit.courtieu
2012-11-15Fixing emacs diff bug with .dir-locals.el.courtieu
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-07Fix reference_or_constr grammar rule to accept @t as a constrgareuselesinge
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-29Fixed #2926:ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-15Egramml: minor simplificationletouzey
2012-10-06restore compatibility with camlp5 < 6.00letouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-05Fix a confusion between types of locations in an untyped part of the parserletouzey
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-02avoid referring to Term in constrexpr.mli and glob_term.mliletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:35:36 +0000