From e3b9244d081bd83af4fcb17214847f8e0e4bc2a3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Jul 2014 17:20:30 +0200
Subject: In setoid_rewrite, force resolution of the contraints generated by
 rewriting only. Do not mix it with resolution of user-introduced subgoals of
 typeclass type (bug found in ATBR).

---
 tactics/rewrite.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7b8b0cc55c..171b1f75a8 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1322,9 +1322,10 @@ let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
 	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
 
 let solve_constraints env (evars,cstrs) =
-  Typeclasses.resolve_typeclasses env ~split:false ~fail:true 
-    (Typeclasses.mark_resolvables ~filter:(all_constraints cstrs) evars)
-
+  let filter = all_constraints cstrs in
+    Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true 
+      (Typeclasses.mark_resolvables ~filter evars)
+      
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 
-- 
cgit v1.2.3