aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29