aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
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-22Make names in [Proofview_monad] more uniform.Arnaud Spiwack
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.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-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-22Remove duplicate code.Arnaud Spiwack
2014-10-21Removing dead code in Rewrite.Pierre-Marie Pédrot
2014-10-21Small invariants in Rewrite code.Pierre-Marie Pédrot
2014-10-21Fixing decompose_app_rel in Rewrite.Pierre-Marie Pédrot
2014-10-21Using new clausenv in rewrite.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 01:25:32 +0000