aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
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-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
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-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-02Fixing 1177da327 (reorganization of the test for generic selection ofHugo Herbelin
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-27Ensuring compatibility when an hypothesis used for destruct isHugo Herbelin
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-22Refine tactic: simplify the conclusion only at the end of the tactic.Arnaud Spiwack
2014-10-22Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Arnaud Spiwack
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-22Remove duplicate code.Arnaud Spiwack
2014-10-20Removing re-typecheking from "refine" in no-check mode of the newHugo Herbelin
2014-10-17Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Hugo Herbelin
2014-10-17Essai où assert_style n'est utilisé que si pas visuellement une équation;Hugo Herbelin
2014-10-16Relaxing again the test on types of replacements in tactic changeHugo Herbelin
2014-10-16In convert_concl/convert_hyp: nf_enter -> enter.Hugo Herbelin
2014-10-16Refresh to avoid algebraic universes on the right.Matthieu Sozeau
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
2014-10-13Fixing "change" and "fold" after convert_hyp/convert_concl moved toHugo Herbelin
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-10-09Propagating name of goal to main subgoal in cut and conversion tactics.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:12:23 +0000