Revert "While resolving typeclass evars in clenv, touch only the ones that appear in the"

This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8.

Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.

2 files changed, 2 insertions, 29 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index bbf7c27fd9..99ea2300c5 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,21 +59,15 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-let clenv_evars clenv value =
-  let templset = Evar.Set.union (Evarutil.evars_of_term value)
-    (Evarutil.evars_of_term (clenv_type clenv))
-  in fun ev _ -> Evar.Set.mem ev templset
-
 let clenv_refine with_evars ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let value = clenv_value clenv in
   let evd' =
     if with_classes then
-      let evd' = Typeclasses.resolve_typeclasses ~filter:(clenv_evars clenv value)
+      let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
         ~fail:(not with_evars) clenv.env clenv.evd
       in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
     else clenv.evd
@@ -81,7 +75,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv value)) gl
+    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
   end
 
 open Unification
diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v
deleted file mode 100644
index 6f89ef6db7..0000000000
--- a/test-suite/bugs/closed/3633.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Set Typeclasses Strict Resolution.
-Class Contr (A : Type) := { center : A }.
-Definition foo {A} `{Contr A} : A.
-Proof.
-  apply center.
-  Undo.
-  (* Ensure the constraints are solved indepentently, otherwise a frozen ?A 
-  makes a search for Contr ?A fail when finishing to apply (fun x => x) *)
-  apply (fun x => x), center. 
-
-(* Toplevel input, characters 7-17:
-Error:
-Unable to satisfy the following constraints:
-In environment:
-A : Type
-H : Contr A
-
-?A : "Type"
-?Contr : "Contr ?X8"
-
- *)
\ No newline at end of file