aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
...
* Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Gravatar Hugo Herbelin2014-11-30
* Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Gravatar Hugo Herbelin2014-11-30
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Used an evar name based on the local def name in "evar" tactic.Gravatar Hugo Herbelin2014-11-25
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
* Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutGravatar Hugo Herbelin2014-11-23
* Specific printer of Evar.Set.t for ocamldebug + more information inGravatar Hugo Herbelin2014-11-22
* Attempt to organize and document unification flags of setoid rewrite.Gravatar Hugo Herbelin2014-11-22
* In setoid_rewrite error messages:Gravatar Hugo Herbelin2014-11-22
* Further simplifying functional induction.Gravatar Hugo Herbelin2014-11-22
* Simplifying code of functional induction.Gravatar Hugo Herbelin2014-11-22
* Not using an (arbitrary) pivot anymore for re-introduction ofGravatar Hugo Herbelin2014-11-22
* New simplification of code for generalizing hypotheses in destruct.Gravatar Hugo Herbelin2014-11-22
* Removing a hack which, according to the comment, should not be necessaryGravatar Hugo Herbelin2014-11-22
* Fix resolve_morphism to build well-scoped terms in case some argumentsGravatar Matthieu Sozeau2014-11-22
* Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing intro_replacing in the new monad.Gravatar Pierre-Marie Pédrot2014-11-22
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing the previous commit. We had to normalize evars first.Gravatar Pierre-Marie Pédrot2014-11-20
* Somehow fixing a side-effect bug in tactics-in-terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Re-removing the Hiddentac module. For some reason it had been reintroducedGravatar Pierre-Marie Pédrot2014-11-20
* Global.env chasing in Inv.Gravatar Pierre-Marie Pédrot2014-11-20
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr]-s in [idtac] messages.Gravatar Arnaud Spiwack2014-11-19
* Tentative rephrasing of error message for rewrite.Gravatar Hugo Herbelin2014-11-18
* Hopefully the last word on having "simpl f" complying with theGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Renouncing to check only at the end of the call to "apply in" theGravatar Hugo Herbelin2014-11-11
* Replugging hints in rewriting strategies.Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3803.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing the unused boolean flag from the move tactic implementation.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
* Granting #3717 (more informative error message on missing arguments for funct...Gravatar Hugo Herbelin2014-11-07
* Fixing #3562 ("as" in "destruct" expects either a disjunctiveGravatar Hugo Herbelin2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Print [rename] tactic properly in info trace.Gravatar Arnaud Spiwack2014-11-07
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Dependency bug in using eqn for destruct.Gravatar Hugo Herbelin2014-11-06
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:19:34 +0000