aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacenv.ml
AgeCommit message (Expand)Author
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-02 01:10:03 +0000