aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
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-15Fix for bug #3618.Matthieu Sozeau
2014-10-15Remaining tactics of the Auto module were put in the monad.Pierre-Marie Pédrot
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-10Fix segfault in native compiler on int31 division.Maxime Dénès
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-08Forgotten hints.ml{,i} files in 38b34dfffcc.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-07Removing debugging information committed by mistake.Hugo Herbelin
2014-10-06Make tclEFFECTS also update the env in the proof monadEnrico Tassi
2014-10-05Semantic fix of a refine in Rewrite.Pierre-Marie Pédrot
2014-10-05Check compatibility of types in change depending on whether it is aHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 15:56:23 +0000