aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Added a CString module.Gravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Continue killing hidden tactics : no more generated h_xxxGravatar letouzey2012-10-15
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* cosmetic concerning interp of TacShowHypsGravatar letouzey2012-10-06
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Adapt pieces of code needing -rectypesGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Revert r15851 "En cours pour bug 2836".Gravatar herbelin2012-10-04
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
* En cours pour bug 2836Gravatar herbelin2012-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
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* 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
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Dump references in reduction tacticsGravatar pboutill2012-08-05
* Dump referencesGravatar pboutill2012-08-05
* Reductionops refactoringGravatar pboutill2012-07-20
* Fix typeclass error handling which was sometimes raising a Failure ("hd").Gravatar msozeau2012-07-11
* Better treatment of error messages in rewrite (avoid use of Errors.print).Gravatar msozeau2012-07-10
* 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
* Fix order of introduction of hints to preserve most-recent-first semantics.Gravatar msozeau2012-07-06
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fixes in rewriting by strategies (almost ready to be documented!):Gravatar msozeau2012-07-05
* Fixing previous commit.Gravatar ppedrot2012-06-28
* Fixing info_auto / info_trivial display.Gravatar ppedrot2012-06-28
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...Gravatar msozeau2012-06-19
* Replacing some str with strbrkGravatar ppedrot2012-06-04