Fix for bug #3618.

Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.

1 files changed, 0 insertions, 100 deletions

diff --git a/test-suite/bugs/opened/3618.v b/test-suite/bugs/opened/3618.v
deleted file mode 100644
index bd24c7a7d7..0000000000
--- a/test-suite/bugs/opened/3618.v
+++ /dev/null
@@ -1,100 +0,0 @@
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-Definition concat {A} {x y z : A} : x = y -> y = z -> x = z. Admitted.
-Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. Admitted.
-Notation "p @ q" := (concat p q) (at level 20).
-Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. Admitted.
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. Admitted.
-
-Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
-  equiv_inv : B -> A ;
-  eisretr : forall x, f (equiv_inv x) = x;
-  eissect : forall x, equiv_inv (f x) = x
-}.
-
-Class Contr_internal (A : Type).
-
-Inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index -> trunc_index.
-
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
-  match n with
-    | minus_two => Contr_internal A
-    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
-  end.
-
-Class IsTrunc (n : trunc_index) (A : Type) : Type :=
-  Trunc_is_trunc : IsTrunc_internal n A.
-Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
-: IsTrunc n (x = y).
-Admitted.
-
-Class Funext.
-
-Instance isequiv_compose A B C f g `{IsEquiv A B f} `{IsEquiv B C g}
-  : IsEquiv (compose g f) | 1000.
-Admitted.
-
-Section IsEquivHomotopic.
-  Context (A B : Type) `(f : A -> B) `(g : A -> B) `{IsEquiv A B f} (h : forall x:A, f x = g x).
-  Let sect := (fun b:B => inverse (h (@equiv_inv _ _ f _ b)) @ @eisretr _ _ f _ b).
-  Let retr := (fun a:A => inverse (ap (@equiv_inv _ _ f _) (h a)) @ @eissect _ _ f _ a).
-  Global Instance isequiv_homotopic : IsEquiv g | 10000
-    := ( BuildIsEquiv _ _ g (@equiv_inv _ _ f _) sect retr).
-End IsEquivHomotopic.
-
-Instance trunc_succ A n `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000. Admitted.
-
-Global Instance trunc_forall A n `{P : A -> Type} `{forall a, IsTrunc n (P a)}
-  : IsTrunc n (forall a, P a) | 100.
-Admitted.
-
-Instance trunc_prod A B n `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) | 100.
-Admitted.
-
-Global Instance trunc_arrow n {A B : Type} `{IsTrunc n B} : IsTrunc n (A -> B) | 100.
-Admitted.
-
-Instance isequiv_pr1_contr {A} {P : A -> Type} `{forall a, IsTrunc minus_two (P a)}
-: IsEquiv (@projT1 A P) | 100.
-Admitted.
-
-Instance trunc_sigma n A `{P : A -> Type} `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
-: IsTrunc n (sigT P) | 100.
-Admitted.
-
-Global Instance trunc_trunc `{Funext} A m n : IsTrunc (trunc_S n) (IsTrunc m A) | 0.
-Admitted.
-
-Definition BiInv {A B} (f : A -> B) : Type
-:= ( {g : B -> A & forall x, g (f x) = x} * {h : B -> A & forall x, f (h x) = x}).
-
-Global Instance isprop_biinv {A B} (f : A -> B) : IsTrunc (trunc_S minus_two) (BiInv f) | 0.
-Admitted.
-
-Instance isequiv_path {A B : Type} (p : A = B)
-: IsEquiv (transport (fun X:Type => X) p) | 0.
-Admitted.
-
-Class ReflectiveSubuniverse_internal :=
-  { inO_internal : Type -> Type ;
-    O : Type -> Type ;
-    O_unit : forall T, T -> O T }.
-
-Class ReflectiveSubuniverse :=
-  ReflectiveSubuniverse_wrap : Funext -> ReflectiveSubuniverse_internal.
-Global Existing Instance ReflectiveSubuniverse_wrap.
-
-Class inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) :=
-  isequiv_inO : inO_internal T.
-
-Global Instance hprop_inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) : IsTrunc (trunc_S minus_two) (inO T) .
-Admitted.
-
-Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
-           (P Q : Type) {Q_inO : inO_internal Q}
-: IsEquiv (fun f => compose f (O_unit P))
-:= _.
-