aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 16:08:53 +0000