aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-10-03Fixing #3657 (check that both sides of a "change with" have the sameHugo Herbelin
2014-10-02Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Hugo Herbelin
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-10-01Made Tacsubst independent of Auto at linking time so that Tacenv doesHugo Herbelin
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-27Changed semantics of induction !id when a clause is given: don'tHugo Herbelin
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-24Added support for interpreting hyp lists in tactic notations.Hugo Herbelin
2014-09-23ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteMatthieu Sozeau
2014-09-23Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingMatthieu Sozeau
2014-09-21Rewrite.apply_lemma is written in state passing style.Pierre-Marie Pédrot
2014-09-21More invariants in the code of Refine.Pierre-Marie Pédrot
2014-09-21Removing a nonsensical Errors.push.Pierre-Marie Pédrot
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 19:04:47 +0000