aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/pptactic.ml
AgeCommit message (Expand)Author
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
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