diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 86bb078296..c6c29a5698 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1195,7 +1195,9 @@ let cutSubstInHyp_LR eqn id gls = let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in if not (dependent (mkRel 1) body) then raise NothingToRewrite; cut_replacing id expected_goal - (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls + (tclTHENFIRST + (bareRevSubstInConcl lbeq body eq) + (refine_no_check (mkVar id))) gls let cutSubstInHyp_RL eqn id gls = (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id) |