11 files changed, 142 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/4612.v b/test-suite/bugs/closed/4612.v
new file mode 100644
index 0000000000..ce95f26acc
--- /dev/null
+++ b/test-suite/bugs/closed/4612.v
@@ -0,0 +1,7 @@
+(* While waiting for support, check at least that it does not raise an anomaly *)
+
+Inductive ctype :=
+| Struct: list ctype -> ctype
+| Bot : ctype.
+
+Fail Scheme Equality for ctype.
diff --git a/test-suite/bugs/closed/4859.v b/test-suite/bugs/closed/4859.v
new file mode 100644
index 0000000000..7be0bedcfc
--- /dev/null
+++ b/test-suite/bugs/closed/4859.v
@@ -0,0 +1,7 @@
+(* Not supported but check at least that it does not raise an anomaly *)
+
+Inductive Fin{n : nat} : Set :=
+| F1{i : nat}{e : n = S i}
+| FS{i : nat}(f : @ Fin i){e : n = S i}.
+
+Fail Scheme Equality for Fin.
diff --git a/test-suite/bugs/closed/8478.v b/test-suite/bugs/closed/8478.v
new file mode 100644
index 0000000000..8baaf8686a
--- /dev/null
+++ b/test-suite/bugs/closed/8478.v
@@ -0,0 +1,11 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Strict Universe Declaration.
+
+Monomorphic Universe v.
+
+Section Foo.
+  Let bar := Type@{u}.
+  Fail Monomorphic Constraint bar.u < v.
+
+End Foo. (* was anomaly undeclared universe due to the constraint *)
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index dfab400baa..cb835ab48d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -64,14 +64,9 @@ In environment
 texpDenote : forall t : type, texp t -> typeDenote t
 t : type
 e : texp t
-t1 : type
-t2 : type
-t0 : type
-b : tbinop t1 t2 t0
-e1 : texp t1
-e2 : texp t2
-The term "0" has type "nat" while it is expected to have type
- "typeDenote t0".
+n : nat
+The term "n" has type "nat" while it is expected to have type
+ "typeDenote ?t@{t1:=Nat}".
 fun '{{n, m, _}} => n + m
      : J -> nat
 fun '{{n, m, p}} => n + m + p
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 926114a1e1..f8f11d7cf6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E}
 (* E M N |=  *)
 
 foo is universe polymorphic
-foo@{Top.16 Top.17 Top.18} = 
-Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
-(* Top.16 Top.17 Top.18 |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Top.17+1,v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
 NonCumulative Inductive Empty@{E} : Type@{E} :=  
@@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v}
 (* v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{k}
+
+For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{u k}
+
+For inseccstr: Argument scope is [type_scope]
 inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -155,24 +163,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.51} -> Type@{axbar'.i}
+axfoo' : Type@{Top.58} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.51} -> Type@{axbar'.i}
+axbar' : Type@{Top.58} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index f806a9f4f7..9aebce1b9a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -122,8 +122,12 @@ Section SomeSec.
   Universe u.
   Definition insec@{v} := Type@{u} -> Type@{v}.
   Print insec.
+
+  Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
+  Print insecind.
 End SomeSec.
 Print insec.
+Print insecind.
 
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 7326f137c2..8a00cd3fe5 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,25 +1,25 @@
 The command has indeed failed with message:
-The user-defined tactic "Top.foo" was not fully applied:
+The user-defined tactic "foo" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There are missing arguments for variables y and _,
 an argument was provided for variable x.
 The command has indeed failed with message:
-The user-defined tactic "Top.baz" was not fully applied:
+The user-defined tactic "baz" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.qux" was not fully applied:
+The user-defined tactic "qux" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.mydo" was not fully applied:
+The user-defined tactic "mydo" was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
@@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.rec" was not fully applied:
+The user-defined tactic "rec" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v
new file mode 100644
index 0000000000..422bb95fdf
--- /dev/null
+++ b/test-suite/ssr/ssrpattern.v
@@ -0,0 +1,7 @@
+Require Import ssrmatching.
+
+Goal forall n, match n with 0 => 0 | _ => 0 end = 0.
+Proof.
+  intro n.
+  ssrpattern (match _ with 0 => _ | S n' => _ end).
+Abort.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ 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/SchemeEquality.v b/test-suite/success/SchemeEquality.v
new file mode 100644
index 0000000000..85d5c3e123
--- /dev/null
+++ b/test-suite/success/SchemeEquality.v
@@ -0,0 +1,29 @@
+(* Examples of use of Scheme Equality *)
+
+Module A.
+Definition N := nat.
+Inductive list := nil | cons : N -> list -> list.
+Scheme Equality for list.
+End A.
+
+Module B.
+  Section A.
+    Context A (eq_A:A->A->bool)
+            (A_bl : forall x y, eq_A x y = true -> x = y)
+            (A_lb : forall x y, x = y -> eq_A x y = true).
+    Inductive I := C : A -> I.
+    Scheme Equality for I.
+  End A.
+End B.
+
+Module C.
+  Parameter A : Type.
+  Parameter eq_A : A->A->bool.
+  Parameter A_bl : forall x y, eq_A x y = true -> x = y.
+  Parameter A_lb : forall x y, x = y -> eq_A x y = true.
+  Hint Resolve A_bl A_lb : core.
+  Inductive I := C : A -> I.
+  Scheme Equality for I.
+  Inductive J := D : list A -> J.
+  Scheme Equality for J.
+End C.
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
index 83fb3d0c8e..241d4eb200 100644
--- a/test-suite/success/attribute-syntax.v
+++ b/test-suite/success/attribute-syntax.v
@@ -1,4 +1,4 @@
-From Coq Require Program.
+From Coq Require Program.Wf.
 
 Section Scope.
 
@@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _.
 
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
+
+Module M.
+  #[local] #[polymorphic] Definition zed := Type.
+
+  #[local, polymorphic] Definition kats := Type.
+End M.
+Check M.zed@{_}.
+Fail Check zed.
+Check M.kats@{_}.
+Fail Check kats.