Forward-port fixes from 8.4 (15358, 15353, 15333).

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

5 files changed, 29 insertions, 8 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 34eb92fa0..524d9d058 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -323,7 +323,7 @@ let coerce_itf loc env isevars v t c1 =
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~with_goals:false ~split:true ~fail:false env evd
+    ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
 (* appliquer le chemin de coercions p à hj *)
 let apply_coercion env sigma p hj typ_cl =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4eeb50cd0..bcd2a1ad1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -109,8 +109,14 @@ let interp_elimination_sort = function
 
 let resolve_evars env evdref fail_evar resolve_classes =
   if resolve_classes then
-    (evdref := Typeclasses.resolve_typeclasses ~with_goals:false
-     ~split:true ~fail:fail_evar env !evdref);
+    (evdref := Typeclasses.resolve_typeclasses 
+     ~filter:(if Flags.is_program_mode () 
+	      then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
+     ~split:true ~fail:fail_evar env !evdref;
+     if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+       evdref := Typeclasses.resolve_typeclasses 
+       ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref;     
+    );
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d76fdc85d..db03112c2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -500,6 +500,15 @@ let has_typeclasses evd =
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
-let resolve_typeclasses ?(with_goals=false) ?(split=true) ?(fail=true) env evd =
+open Evar_kinds
+type evar_filter = Evar_kinds.t -> bool
+
+let all_evars _ = true
+let no_goals = function GoalEvar -> false | _ -> true
+let no_goals_or_obligations = function
+  | GoalEvar | QuestionMark _ -> false
+  | _ -> true
+
+let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses evd) then evd
-  else !solve_instanciations_problem env evd with_goals split fail
+  else !solve_instanciations_problem env evd filter split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 411651afe..b51732547 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -87,7 +87,13 @@ val mark_resolvable : evar_info -> evar_info
 val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
-val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool ->
+(** Filter which evars to consider for resolution. *)
+type evar_filter = Evar_kinds.t -> bool
+val all_evars : evar_filter
+val no_goals : evar_filter
+val no_goals_or_obligations : evar_filter
+
+val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
@@ -102,7 +108,7 @@ val register_remove_instance_hint : (global_reference -> unit) -> unit
 val add_instance_hint : constr -> bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
-val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
+val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
 
 val declare_instance : int option -> bool -> global_reference -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fd40cca7c..eec9b0bc3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -967,7 +967,7 @@ let check_types env flags (sigma,_,_ as subst) m n =
 
 let try_resolve_typeclasses env evd flags m n =
   if flags.resolve_evars then
-    try Typeclasses.resolve_typeclasses ~with_goals:false ~split:false
+    try Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false
 	  ~fail:true env evd
     with e when Typeclasses_errors.unsatisfiable_exception e ->
       error_cannot_unify env evd (m, n)