diff options
| author | msozeau | 2013-06-14 14:50:51 +0000 |
|---|---|---|
| committer | msozeau | 2013-06-14 14:50:51 +0000 |
| commit | 7571dfee41570004e7f236e8b11c18605172eb0e (patch) | |
| tree | 25a27dc1e8e25aa9b07ab4226232ec5aaaf9f7e5 | |
| parent | c9733ae91345b5d720cb361e99625874651a4a6e (diff) | |
When doing setoid_rewrite through rewrite, do resolution of classes
in w_unify_to_subterm, deactivated by previous patch (fixes RelationAlgebra).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16579 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |