Merge branch 'v8.6'

5 files changed, 69 insertions, 39 deletions

diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
new file mode 100644
index 0000000000..b97a8ce640
--- /dev/null
+++ b/test-suite/bugs/closed/4416.v
@@ -0,0 +1,3 @@
+Goal exists x, x.
+unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
+(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 0000000000..e884355fde
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,32 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Proof.
+  intros P H.
+  refine (Build_Decidable _ (if H then true else false) _).
+  intuition congruence.
+Qed.
+
+Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+
+Goal forall (a b : Foo), {a=b}+{a<>b}.
+intros.
+abstract (abstract (decide equality)). (*abstract works here*)
+Qed.
+
+Check ltac:(abstract (exact I)) : True.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split. typeclasses eauto. typeclasses eauto. Qed.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split.
+refine _.
+refine _.
+Defined.
+(*fails*)
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/Case13.v b/test-suite/success/Case13.v
index 356a67efec..8f95484cfd 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,41 +87,3 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
-
-(* Check use of the no-dependency strategy when a type constraint is
-   given (and when the "inversion-and-dependencies-as-evars" strategy
-   is not strong enough because of a constructor with a type whose
-   pattern structure is not refined enough for it to be captured by
-   the inversion predicate) *)
-
-Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
-        match y with
-        | F  => f y H1
-        | G _ => f y H2
-        end : Q y z.
-
-(* Check use of the maximal-dependency-in-variable strategy even when
-   no explicit type constraint is given (and when the
-   "inversion-and-dependencies-as-evars" strategy is not strong enough
-   because of a constructor with a type whose pattern structure is not
-   refined enough for it to be captured by the inversion predicate) *)
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
-        match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end.
-
-(* Check use of the maximal-dependency-in-variable strategy for "Var"
-   variables *)
-
-Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
-intros z P Q y H1 H2 f.
-Show.
-refine (match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end).
-Qed.
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.