aboutsummaryrefslogtreecommitdiff
path: root/ltac/extraargs.ml4
AgeCommit message (Expand)Author
2016-03-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot