aboutsummaryrefslogtreecommitdiff
path: root/grammar/tacextend.ml4
AgeCommit message (Expand)Author
2016-01-20Update copyright headers.Maxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
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-24Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholePierre-Marie Pédrot
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
2014-05-17Fixing Camlp4 compilationPierre-Marie Pédrot
2014-05-16Tactics defined through TACTIC EXTEND that are only defined as a string doPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-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
2014-02-05Tactic extensions do not need to be classified by the STM, asPierre-Marie Pédrot
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-10-23CList.factorize_left with a parametric equalityletouzey
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
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-06-06Uniformizing generic argument types.ppedrot
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2013-03-17Fix some camlp5 quotations , restoring compatibility with camlp5 5.xletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-05More monomorphization.ppedrot
2012-12-14Modulification of identifierppedrot
2012-12-13Using library string functions.ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
2012-10-15Stylistic improvement: avoid a "if match List.hd"letouzey
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
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-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-08-08Updating headers.herbelin
2012-07-12Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)letouzey
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01More cleaningppedrot
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:46:28 +0000