aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Avoid failure in debugger when printing Ltac names.Gravatar herbelin2013-01-27
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* 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