From a8d50dd372fc9365d3f6f21551567f05937d93ef Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 5 Jan 2008 19:10:06 +0000
Subject: Fix a naming bug reported by Arnaud Spiwack, allow instance search to
 create evars and try to solve them too. Finally, rework tactics on setoids
 and design a saturating tactic to help solve goals on any setoid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b0e7cb1470..306ef3a190 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -209,11 +209,9 @@ let instances r =
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
-  if evi.evar_body = Evar_empty then
-    try
-      !solve_instanciation_problem env evd ev evi
-    with Exit -> acc
-  else acc
+  try
+    !solve_instanciation_problem env evd ev evi
+  with Exit -> acc
 
 let resolve_one_typeclass env types =
   try
@@ -280,7 +278,9 @@ let resolve_typeclasses ?(check=true) env sigma evd =
     let (evars', progress) = 
       Evd.fold 
 	(fun ev evi acc -> 
-	  if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) 
+	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
+	    resolve_typeclass env ev evi acc 
+	  else acc) 
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
-- 
cgit v1.2.3