Merge PR #17665: Remove bugged test of leaking evars in class_tactics

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

tactics/class_tactics.ml

@@ -1019,14 +1019,6 @@ module Search = struct
     in
     let finished = Proofview.finished pv' in
     let evm' = Proofview.return pv' in
-    let shelf = Evd.shelf evm' in
-    assert(Evd.fold_undefined (fun ev _ acc ->
-        let okev = Evd.mem evm ev || List.mem ev shelf in
-          if not okev then
-            Feedback.msg_debug
-              (str "leaking evar " ++ int (Evar.repr ev) ++
-                  spc () ++ pr_ev_with_id evm' ev);
-          acc && okev) evm' true);
     let _, evm' = Evd.pop_future_goals evm' in
     let () = ppdebug 1 (fun () ->
         str"Finished resolution with " ++ str(if finished then "a complete" else "an incomplete") ++

test-suite/bugs/bug_5243.v

@@ -0,0 +1,38 @@
+Typeclasses eauto := debug.
+
+Class Foo A := foo : A.
+
+Hint Extern 0 (Foo _) => lazy beta delta; give_up : typeclass_instances.
+
+Lemma t A : A.
+  notypeclasses refine ((_ : Foo A)).
+  typeclasses eauto.
+
+(*
+No more subgoals, but there are some goals you gave up:
+
+A
+
+You need to go back and solve them.
+*)
+
+Abort.
+
+Lemma t A : A.
+  refine ((_ : Foo A)).
+
+(*
+1: looking for (Foo A) without backtracking
+1.1: (*external*) (lazy beta delta; give_up) on
+(Foo A), 0 subgoal(s)
+leaking evar 10
+A
+
+Anomaly:
+File "tactics/class_tactics.ml", line 1345, characters 11-17: Assertion failed.
+Please report at http://coq.inria.fr/bugs/.
+ *)
+  Unshelve.
+  all:fail. (* no more goals *)
+  Fail Qed.
+Abort.