aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacenv.ml
AgeCommit message (Expand)Author
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-09-03Fixing bug #2818.Pierre-Marie Pédrot
2014-09-03Useless hooks in Tacintern.Pierre-Marie Pédrot
2014-09-03Code simplification in Tacenv.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.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-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-07-27Code cleaning in Tacenv.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-06-30Useless keeping of dirpath in tactic aliases.Pierre-Marie Pédrot
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-02Removing symmetry from the atomic tactics.Pierre-Marie Pédrot
2014-05-21Allowing Ltac definitions that may be unusable because of a built-inPierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:33:51 +0000