Fix bugs related to Program integration.

- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 1 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4a850db669..125ef94dcc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -635,6 +635,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 *)
 
@@ -645,7 +662,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