aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-11-25Used an evar name based on the local def name in "evar" tactic.Hugo Herbelin
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-23Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutHugo Herbelin
2014-11-22Specific printer of Evar.Set.t for ocamldebug + more information inHugo Herbelin
2014-11-22Attempt to organize and document unification flags of setoid rewrite.Hugo Herbelin
2014-11-22In setoid_rewrite error messages:Hugo Herbelin
2014-11-22Further simplifying functional induction.Hugo Herbelin
2014-11-22Simplifying code of functional induction.Hugo Herbelin
2014-11-22Not using an (arbitrary) pivot anymore for re-introduction ofHugo Herbelin
2014-11-22New simplification of code for generalizing hypotheses in destruct.Hugo Herbelin
2014-11-22Removing a hack which, according to the comment, should not be necessaryHugo Herbelin
2014-11-22Fix resolve_morphism to build well-scoped terms in case some argumentsMatthieu Sozeau
2014-11-22Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Pierre-Marie Pédrot
2014-11-22Writing intro_replacing in the new monad.Pierre-Marie Pédrot
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-20Fixing the previous commit. We had to normalize evars first.Pierre-Marie Pédrot
2014-11-20Somehow fixing a side-effect bug in tactics-in-terms.Pierre-Marie Pédrot
2014-11-20Re-removing the Hiddentac module. For some reason it had been reintroducedPierre-Marie Pédrot
2014-11-20Global.env chasing in Inv.Pierre-Marie Pédrot
2014-11-20Adding locations to tclZEROMSG.Pierre-Marie Pédrot
2014-11-19Print [uconstr]-s in [idtac] messages.Arnaud Spiwack
2014-11-18Tentative rephrasing of error message for rewrite.Hugo Herbelin
2014-11-18Hopefully the last word on having "simpl f" complying with theHugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-14Preserving the good effect of 014e5ac92a on not leaving dangling localHugo Herbelin
2014-11-13Removing yet another source of remaining local definitions.Hugo Herbelin
2014-11-11Renouncing to check only at the end of the call to "apply in" theHugo Herbelin
2014-11-10Replugging hints in rewriting strategies.Pierre-Marie Pédrot
2014-11-10Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Pierre-Marie Pédrot
2014-11-09Fixing bug #3803.Pierre-Marie Pédrot
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-08Compatibility with 8.4 in the heuristic used to build the inductionHugo Herbelin
2014-11-07Granting #3717 (more informative error message on missing arguments for funct...Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-07Print [rename] tactic properly in info trace.Arnaud Spiwack
2014-11-06Restoring clear_flag (thanks a lot to jonikelee to notice it).Hugo Herbelin
2014-11-06Optimizing when to clear generalized hypotheses in destruct.Hugo Herbelin
2014-11-06Dependency bug in using eqn for destruct.Hugo Herbelin
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-11-03Subtle swap of lines to preserve VarInstance src field before checkingHugo Herbelin
2014-11-03Fix to 844431761 on improving elimination with indices, getting rid ofHugo Herbelin
2014-11-02Saving some nf_evars in the code of destruct/induction.Hugo Herbelin
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 09:47:29 +0000