Merge branch 'v8.5' into v8.6

2 files changed, 34 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v
new file mode 100644
index 0000000000..bcde510ee6
--- /dev/null
+++ b/test-suite/bugs/closed/5123.v
@@ -0,0 +1,33 @@
+(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *)
+
+(*Pose an open constr to prevent immediate typeclass resolution in holes:*)
+Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H.
+
+Inductive vect A : nat -> Type :=
+| vnil : vect A 0
+| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n).
+
+Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
+
+Require Bool.
+
+Instance Bool_eqdec : Eqdec bool := Bool.bool_dec.
+
+Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}.
+
+Typeclasses eauto := debug.
+
+Goal True.
+  unshelve opose (@vect_sigT_eqdec _ _ _ _) as H.
+  all:cycle 2.
+  eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*)
+  Focus 5.
+Abort.
+
+Goal True.
+  opose (@vect_sigT_eqdec _ _ _ _) as H.
+  Unshelve.
+  all:cycle 3.
+  eapply existT. (*This does no typeclass resultion, which is correct.*)
+  Focus 5.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index dfa438d90a..3eaa04144f 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,7 +5,7 @@ Record Equ (A : Type) (R : A -> A -> Prop).
 Definition equiv {A} R (e : Equ A R) := R.
 Record Refl (A : Type) (R : A -> A -> Prop).
 Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
-Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo.
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
 
 Variable R : nat -> nat -> Prop.
 Lemma bas : Equ nat R.