aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-11-02Some reorganization of the code for destruct/induction:Hugo Herbelin
2014-11-02Plural and singular forms in error messages.Hugo Herbelin
2014-11-02Fixing 1177da327 (reorganization of the test for generic selection ofHugo Herbelin
2014-11-01Info: the warning message of the defunct [info] tactic now points to the [Inf...Arnaud Spiwack
2014-11-01Info: print name of calls to Ltac constants ([TacCall]).Arnaud Spiwack
2014-11-01Info: tactic notations (TacAlias) print their names.Arnaud Spiwack
2014-11-01Info: Tactics coming from [TACTIC EXTEND] print their names.Arnaud Spiwack
2014-11-01Info: print the name of atomic tactics.Arnaud Spiwack
2014-11-01Info: Ltac's idtac logs its message in the info trace.Arnaud Spiwack
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-31Avoid "destruct H" to apply on H itself when H is a section variable.Hugo Herbelin
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-27Removing the last Evd.diff from Hints.Pierre-Marie Pédrot
2014-10-27Making destruct on idents with maximal implicit arguments working, byHugo Herbelin
2014-10-27Ensuring compatibility when an hypothesis used for destruct isHugo Herbelin
2014-10-27Fixing evars lost in interpretation of eliminator of destruct.Hugo Herbelin
2014-10-26Preventing potential evar leak in Rewrite.Pierre-Marie Pédrot
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-26Dead code + typo.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-24Apparently, the former refine was simplifying in hypotheses too.Hugo Herbelin
2014-10-24Addressing report #3279 (inconsistency of behavior of the -> and <-Hugo Herbelin
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Refine tactic: simplify the conclusion only at the end of the tactic.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 07:33:42 +0000