aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Printing function for Stdargs in debuggerGravatar Pierre Boutillier2013-12-19
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Synchronizing the printer of tactic notations.Gravatar ppedrot2013-11-13
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* Update comments.Gravatar aspiwack2013-11-02
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
* Adds a tactical once.Gravatar aspiwack2013-11-02
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Adding genarg printer to debugger.Gravatar ppedrot2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Pptactic.pr_raw_tactic is now without env argumentGravatar letouzey2013-03-14
* More monomorphization.Gravatar ppedrot2013-03-05
* 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