13 files changed, 92 insertions, 59 deletions
diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v
new file mode 100644
index 0000000000..f0162f3b27
--- /dev/null
+++ b/test-suite/bugs/closed/2245.v
@@ -0,0 +1,11 @@
+Module Type Test.
+
+Section Sec.
+Variables (A:Type).
+Context (B:Type).
+End Sec.
+
+Fail Check B. (* used to be found !!! *)
+Fail Check A.
+
+End Test.
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 85ad41d1cf..23a58501f3 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -505,8 +505,6 @@ Qed.
 Require Export Coq.Logic.FunctionalExtensionality.
 Print PLanguage.
 
-Unset Standard Proposition Elimination Names.
-
 Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
 Transformation (PLanguage l1) (PLanguage l2) :=
   mkTransformation (PLanguage l1) (PLanguage l2)
diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
index 89d476dcb1..38f03b166b 100644
--- a/test-suite/bugs/closed/3481.v
+++ b/test-suite/bugs/closed/3481.v
@@ -3,7 +3,7 @@ Set Implicit Arguments.
 
 Require Import Logic.
 Module NonPrim.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Record prodwithlet (A B : Type) : Type :=
   pair' { fst : A; fst' := fst; snd : B }.
 
@@ -21,7 +21,7 @@ End NonPrim.
 
 Global Set Universe Polymorphism.
 Global Set Asymmetric Patterns.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Local Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index 5adc48215e..1f0f3b0da9 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end; unfold Basics.flip.
   Focus 2.
-  Set Typeclasses Debug.
-  Set Typeclasses Legacy Resolution.
-  apply reflexivity.
-  (* Debug: 1.1: apply @IsPointed_catOP on
-(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
-Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
-Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
-Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
-Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
-Debug: Backtracking after apply @Equivalence_Reflexive
-Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
-Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
-Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
-*)
-  Undo. Unset Typeclasses Legacy Resolution.
-  Test Typeclasses Unique Solutions.
-  Test Typeclasses Unique Instances.
-  Show Existentials.
-  Set Typeclasses Debug Verbosity 2.
-  Set Printing All.
   (* As in 8.5, allow a shelved subgoal to remain *)
   apply reflexivity.
   
diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v
index c981207e6b..ea122e521f 100644
--- a/test-suite/bugs/closed/3520.v
+++ b/test-suite/bugs/closed/3520.v
@@ -3,7 +3,7 @@ Set Primitive Projections.
 Record foo (A : Type) := 
   { bar : Type ; baz := Set; bad : baz = bar }.
 
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 
 Record notprim : Prop :=
   { irrel : True; relevant : nat }.
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
index bd53389b4f..b8754bce98 100644
--- a/test-suite/bugs/closed/3662.v
+++ b/test-suite/bugs/closed/3662.v
@@ -1,6 +1,6 @@
 Set Primitive Projections.
 Set Implicit Arguments.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Record prod A B := pair { fst : A ; snd : B }.
 Definition f : Set -> Type := fun x => x.
 
diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v
new file mode 100644
index 0000000000..4d263c5a82
--- /dev/null
+++ b/test-suite/bugs/closed/6313.v
@@ -0,0 +1,64 @@
+(* Former open goals in nested proofs were lost *)
+
+(* This used to fail with "Incorrect number of goals (expected 1 tactic)." *)
+
+Inductive foo := a | b | c.
+Goal foo -> foo.
+  intro x.
+  simple refine (match x with
+                 | a => _
+                 | b => ltac:(exact b)
+                 | c => _
+                 end); [exact a|exact c].
+Abort.
+
+(* This used to leave the goal on the shelf and fails at reflexivity *)
+
+Goal (True/\0=0 -> True) -> True.
+  intro f.
+  refine
+   (f ltac:(split; only 1:exact I)).
+  reflexivity.
+Qed.
+
+(* The "Unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f (b:comparison) : b=b.
+refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+exact (eq_refl Gt).
+Unshelve.
+exact (eq_refl Eq).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
+
+(* The "Unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f2 (b:comparison) : b=b.
+refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+Unshelve. (* Note: Unshelve puts goals at the end *)
+exact (eq_refl Gt).
+exact (eq_refl Eq).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
+
+(* The "unshelve" used to not see the explicitly "shelved" goal *)
+
+Lemma f3 (b:comparison) : b=b.
+unshelve refine (match b with
+   Eq => ltac:(shelve)
+ | Lt => ltac:(give_up)
+ | Gt => _
+ end).
+(* Note: unshelve puts goals at the beginning *)
+exact (eq_refl Eq).
+exact (eq_refl Gt).
+Fail auto. (* Check that there are no more regular subgoals *)
+Admitted.
diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v
new file mode 100644
index 0000000000..7f33afcc2f
--- /dev/null
+++ b/test-suite/bugs/closed/6634.v
@@ -0,0 +1,6 @@
+From Coq Require Import ssreflect.
+
+Lemma normalizeP (p : tt = tt) : p = p.
+Proof.
+Fail move: {2} tt p.
+Abort.
diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v
new file mode 100644
index 0000000000..5167a5364a
--- /dev/null
+++ b/test-suite/bugs/closed/6910.v
@@ -0,0 +1,5 @@
+From Coq Require Import ssreflect ssrfun.
+
+(* We should be able to use Some_inj as a view: *)
+Lemma foo (x y : nat) : Some x = Some y -> x = y.
+Proof. by move/Some_inj. Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index 017780c1f3..f69c71a026 100644
--- a/test-suite/bugs/closed/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -3,7 +3,7 @@ Set Implicit Arguments.
 Require Import Logic.
 
 Set Asymmetric Patterns.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v
index 5bb7fa8c12..a6ff78d127 100644
--- a/test-suite/bugs/closed/HoTT_coq_104.v
+++ b/test-suite/bugs/closed/HoTT_coq_104.v
@@ -4,7 +4,7 @@ Require Import Logic.
 
 Global Set Universe Polymorphism.
 Global Set Asymmetric Patterns.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Local Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 0b576db6b3..820022d995 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -2,7 +2,6 @@ Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
-Unset Standard Proposition Elimination Names.
 
 Set Keyed Unification.
 
diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v
deleted file mode 100644
index cfad763572..0000000000
--- a/test-suite/bugs/opened/3926.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Notation compose := (fun g f x => g (f x)).
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Arguments idpath {A a} , [A] a.
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-Local Open Scope equiv_scope.
-Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x.
-Generalizable Variables A B C f g.
-Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000
-  := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1).
-Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g
-  := Build_IsEquiv _ _ g (f ^-1).
-Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000
-  := Build_IsEquiv B A f^-1 f.
-Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}
-  `{IsEquiv A B f} `{IsEquiv A C (g o f)}
-  : IsEquiv g.
-Proof.
-  Unset Typeclasses Modulo Eta.
-  exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))) || fail "too early".
-  Undo.
-  Set Typeclasses Modulo Eta.
-  Set Typeclasses Dependency Order.
-  Set Typeclasses Debug.
-  Fail exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))).