4 files changed, 71 insertions, 12 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index faba5c7563..521fa2247b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,22 +183,26 @@ type inference_flags = {
   expand_evars : bool
 }
 
+let frozen_holes (sigma, sigma') =
+  let fold evk _ accu = Evar.Set.add evk accu in
+  Evd.fold_undefined fold sigma Evar.Set.empty
+
 let pending_holes (sigma, sigma') =
   let fold evk _ accu =
     if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
   in
   Evd.fold_undefined fold sigma' Evar.Set.empty
 
-let apply_typeclasses env evdref pending fail_evar =
-  let filter_pending evk = Evar.Set.mem evk pending in
+let apply_typeclasses env evdref frozen fail_evar =
+  let filter_frozen evk = Evar.Set.mem evk frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
-	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk)
-              else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk))
+	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
+              else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
      ~split:true ~fail:fail_evar env !evdref;
   if Flags.is_program_mode () then (* Try optionally solving the obligations *)
     evdref := Typeclasses.resolve_typeclasses
-      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref
+      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
 
 let apply_inference_hook hook evdref pending =
   evdref := Evar.Set.fold (fun evk sigma ->
@@ -219,9 +223,9 @@ let apply_heuristics env evdref fail_evar =
   with e when Errors.noncritical e ->
     let e = Errors.push e in if fail_evar then iraise e
 
-let check_typeclasses_instances_are_solved env current_sigma pending =
+let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env (ref current_sigma) pending true
+  apply_typeclasses env (ref current_sigma) frozen true
 
 let check_extra_evars_are_solved env current_sigma pending =
   Evar.Set.iter
@@ -233,26 +237,28 @@ let check_extra_evars_are_solved env current_sigma pending =
 	| _ ->
 	    error_unsolvable_implicit loc env current_sigma evk None) pending
 
-let check_evars_are_solved env current_sigma pending =
-  check_typeclasses_instances_are_solved env current_sigma pending;
+let check_evars_are_solved env current_sigma frozen pending =
+  check_typeclasses_instances_are_solved env current_sigma frozen;
   check_problems_are_solved env current_sigma;
   check_extra_evars_are_solved env current_sigma pending
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
   let evdref = ref current_sigma in
-  if flags.use_typeclasses then apply_typeclasses env evdref pending false;
+  if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
     apply_inference_hook (Option.get flags.use_hook env) evdref pending;
   if flags.use_unif_heuristics then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref pending;
+  if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
 let check_evars_are_solved env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
-  check_evars_are_solved env current_sigma pending
+  check_evars_are_solved env current_sigma frozen pending
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
   let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v
index a03e8ffdab..a03e8ffdab 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/closed/3848.v
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 0000000000..3cdc4ada02
--- /dev/null
+++ b/test-suite/bugs/closed/4256.v
@@ -0,0 +1,43 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Global Set Universe Polymorphism.
+Monomorphic Universe i.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Notation "-1" := (trunc_S minus_two) (at level 0).
+
+Class IsPointed (A : Type) := point : A.
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+Coercion pointed_type : pType >-> Sortclass.
+Existing Instance ispointed_type.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+
+
+Record ooGroup :=
+  { classifying_space : pType@{i} }.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+  (** This works: *)
+  pose (x0 := point X).
+  pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
+  clear H x0.
+  (** But this doesn't: *)
+  pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 0000000000..f988539d62
--- /dev/null
+++ b/test-suite/bugs/closed/4484.v
@@ -0,0 +1,10 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Class A := {}.
+Axiom foo : forall {ac : A}, bool.
+Lemma bar (ac : A) : True.
+Check (match foo as k return foo = k -> True with
+       | true => _
+       | false => _
+       end eq_refl).