diff options
| -rw-r--r-- | tactics/rewrite.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 679fc8da67..a678a4e306 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1887,16 +1887,17 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl = (* ~flags:(false,true) to allow to mark occurrences that must not be rewritten simply by replacing them with let-defined definitions in the context *) - Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env + Unification.w_unify_to_subterm + ~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env cl.evd ((if l2r then c1 else c2),but) with Pretype_errors.PretypeError _ -> (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) - Unification.w_unify_to_subterm ~flags:flags + Unification.w_unify_to_subterm + ~flags:{ flags with Unification.resolve_evars = true } env cl.evd ((if l2r then c1 else c2),but) in - let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in let cl' = {cl with evd = evd'} in let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in let nf c = Evarutil.nf_evar cl'.evd (Clenv.clenv_nf_meta cl' c) in |