From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 tactics/class_tactics.ml4 | 37 +++++++++++++++++++++++++------------
 1 file changed, 25 insertions(+), 12 deletions(-)

(limited to 'tactics/class_tactics.ml4')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 42df244d..e063124d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -634,6 +634,23 @@ let has_undefined p oevd evd =
     snd (p oevd ev evi))
     evd false
 
+(** Revert the resolvability status of evars after resolution,
+    potentially unprotecting some evars that were set unresolvable
+    just for this call to resolution. *)
+
+let revert_resolvability oevd evd = 
+  Evd.fold_undefined
+    (fun ev evi evm ->
+     try 
+       if not (Typeclasses.is_resolvable evi) then
+	 let evi' = Evd.find_undefined oevd ev in
+	   if Typeclasses.is_resolvable evi' then
+	     Evd.add evm ev (Typeclasses.mark_resolvable evi)
+	   else evm
+       else evm
+     with Not_found -> evm)
+  evd evd
+
 (** If [do_split] is [true], we try to separate the problem in
     several components and then solve them separately *)
 
@@ -644,7 +661,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
   let in_comp comp ev = if do_split then Intset.mem ev comp else true
   in
   let rec docomp evd = function
-    | [] -> evd
+    | [] -> revert_resolvability oevd evd
     | comp :: comps ->
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
@@ -659,24 +676,20 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  docomp evd comps
   in docomp oevd split
 
-let initial_select_evars onlyargs =
-  if onlyargs then
-    (fun evd ev evi ->
-      Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd))
-      && Typeclasses.is_class_evar evd evi)
-  else
-    (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
+let initial_select_evars filter evd ev evi =
+  filter (snd evi.Evd.evar_source) &&
+  Typeclasses.is_class_evar evd evi
 
-let resolve_typeclass_evars debug m env evd onlyargs split fail =
+let resolve_typeclass_evars debug m env evd filter split fail =
   let evd = 
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with _ -> evd
   in
-    resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
+    resolve_all_evars debug m env (initial_select_evars filter) evd split fail
 
-let solve_inst debug depth env evd onlyargs split fail =
-  resolve_typeclass_evars debug depth env evd onlyargs split fail
+let solve_inst debug depth env evd filter split fail =
+  resolve_typeclass_evars debug depth env evd filter split fail
 
 let _ =
   Typeclasses.solve_instanciations_problem :=
-- 
cgit v1.2.3