aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
2014-09-15Ltac names in binders: some Ltac values can be seen both as terms and identif...Arnaud Spiwack
2014-09-15A small pass of code cleaning and clenv removing in Rewrite.Pierre-Marie Pédrot
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-15Removing one Evd.merge in Rewrite.Pierre-Marie Pédrot
2014-09-15More invariants in Rewrite unification.Pierre-Marie Pédrot
2014-09-15The unifying functions of Rewrite uses the return types of strategies.Pierre-Marie Pédrot
2014-09-15Splitting the uses of the unification function according to the status ofPierre-Marie Pédrot
2014-09-14Rewrite.apply_strategy uses the same return type as strategies.Pierre-Marie Pédrot
2014-09-14Proper type for rewrite strategy results.Pierre-Marie Pédrot
2014-09-13Retroknowledge arguments are made VERNAC ARGUMENTS.Pierre-Marie Pédrot
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 09:37:41 +0000