aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/pptactic.ml
AgeCommit message (Expand)Author
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot