diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 1e3996429..c79f8b35f 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1324,12 +1324,13 @@ module Strategies = let reduce (r : Redexpr.red_expr) : 'a pure_strategy = fun state env avoid t ty cstr evars -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in - let t' = rfn env (goalevars evars) t in + let evars', t' = rfn env (goalevars evars) t in if eq_constr t' t then state, Identity else state, Success { rew_car = ty; rew_from = t; rew_to = t'; - rew_prf = RewCast ckind; rew_evars = evars } + rew_prf = RewCast ckind; + rew_evars = evars', cstrevars evars } let fold_glob c : 'a pure_strategy = fun state env avoid t ty cstr evars -> |