aboutsummaryrefslogtreecommitdiff
path: root/grammar/tacextend.ml4
AgeCommit message (Expand)Author
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey
2016-05-31Making the grammar/ folder independent from the other ones.Pierre-Marie Pédrot
2016-05-14Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Pierre-Marie Pédrot
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-03-20Moving the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-03-19EXTEND macros use their own internal representations.Pierre-Marie Pédrot
2016-03-19Do not keep the argument type in ExtNonTerminal.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-18Making the EXTEND macros almost self-contained.Pierre-Marie Pédrot
2016-03-18ARGUMENT EXTEND made of only one entry share the same grammar.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Reducing the number of modules linked in grammar.cma.Pierre-Marie Pédrot
2016-02-24Removing the Q_coqast module.Pierre-Marie Pédrot
2016-02-01Infering atomic ML entries from their grammar.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Proper datatype for EXTEND syntax tokens.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
2015-01-27Tentative fix for bug #3957.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 04:17:31 +0000