aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Fixing Show Script issues.Gravatar ppedrot2012-09-20
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* 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