aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppannotation.ml
Commit message (Expand)AuthorAge
* Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
* printing/Ppannotation: Introduce a new annotation for keywords.Gravatar Regis-Gianas2014-11-04
* printing/RichPrinter: New API for rich pretty-printing.Gravatar Regis-Gianas2014-11-04
* Ppannotation.t: New constructor AVernac.Gravatar Regis-Gianas2014-11-04
* Ppannotation: New.Gravatar Regis-Gianas2014-11-04