aboutsummaryrefslogtreecommitdiff
path: root/printing/ppannotation.mli
AgeCommit message (Expand)Author
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2016-09-15Made Ppanotation Ltac-agnostic.Pierre-Marie Pédrot
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-04printing/Ppannotation: New annotation for tactic syntactic objects.Regis-Gianas
2014-11-04printing/Ppannotation: Introduce a new annotation for keywords.Regis-Gianas
2014-11-04printing/RichPrinter: New API for rich pretty-printing.Regis-Gianas
2014-11-04Ppannotation.t: New constructor AVernac.Regis-Gianas
2014-11-04Ppannotation: New.Regis-Gianas