aboutsummaryrefslogtreecommitdiff
path: root/parsing/egramcoq.mli
AgeCommit message (Expand)Author
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-05-12Moving the ML tactic extension mechanism to a Libobject-based one.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Moving notation types into grammar rule.ppedrot
2013-11-09Cleaning and documenting Egramcoq.ppedrot
2013-06-27Added a generic handler of Ltac quotations, based on the existingppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
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-08-08Updating headers.herbelin
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:07:47 +0000