aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 11:53:00 +0000