9 files changed, 149 insertions, 10 deletions
diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v
index ed035f5213..2f7425bce6 100644
--- a/test-suite/success/BracketsWithGoalSelector.v
+++ b/test-suite/success/BracketsWithGoalSelector.v
@@ -14,3 +14,12 @@ Proof.
 Fail Qed.
   }
 Qed.
+
+Lemma foo (n: nat) (P : nat -> Prop):
+  P n.
+Proof.
+  intros.
+  refine (nat_ind _ ?[Base] ?[Step] _).
+  [Base]: { admit. }
+  [Step]: { admit. }
+Abort.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 717dc0debe..ebf5b094e1 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -183,3 +183,33 @@ End HintCut.
 Goal forall (m : nat), exists n, m = n /\ m = n.
   intros m; eexists; split; [trivial | reflexivity].
 Qed.
+
+Section HintTransparent.
+
+  Definition fn (x : nat) := S x.
+
+  Create HintDb trans.
+
+  Hint Resolve eq_refl | (_ = _) : trans.
+
+  (* No reduction *)
+  Hint Variables Opaque : trans.  Hint Constants Opaque : trans.
+
+  Goal forall x : nat, fn x = S x.
+  Proof.
+    intros.
+    Fail typeclasses eauto with trans.
+    unfold fn.
+    typeclasses eauto with trans.
+  Qed.
+
+  (** Now allow unfolding fn *)
+  Hint Constants Transparent : trans.
+
+  Goal forall x : nat, fn x = S x.
+  Proof.
+    intros.
+    typeclasses eauto with trans.
+  Qed.
+
+End HintTransparent.
diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v
index b63bead477..bf3a87da25 100644
--- a/test-suite/success/Fourier.v
+++ b/test-suite/success/LraTest.v
@@ -1,12 +1,14 @@
-Require Import Rfunctions.
-Require Import Fourier.
+Require Import Reals.
+Require Import Lra.
+
+Open Scope R_scope.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; fourier.
+intros; split_Rabs; lra.
 Qed.
 
 Lemma l2 :
  forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
 intros.
-split_Rabs; fourier.
+split_Rabs; lra.
 Qed.
diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v
new file mode 100644
index 0000000000..633a5e4749
--- /dev/null
+++ b/test-suite/success/LtacDeprecation.v
@@ -0,0 +1,32 @@
+Set Warnings "+deprecated".
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Ltac foo x := idtac.
+
+Goal True.
+Fail (foo true).
+Abort.
+
+Fail Ltac bar := foo.
+Fail Tactic Notation "bar" := foo.
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Tactic Notation "bar" := idtac.
+
+Goal True.
+Fail bar.
+Abort.
+
+Fail Ltac zar := bar.
+
+Set Warnings "-deprecated".
+
+Ltac zar := foo.
+Ltac zarzar := bar.
+
+Set Warnings "+deprecated".
+
+Goal True.
+zar x.
+zarzar.
+Abort.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 7c2cf3ee52..1b33863e3b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -126,3 +126,31 @@ Notation "'myexists' x , p" := (ex (fun x => p))
   (at level 200, x ident, p at level 200, right associativity) : type_scope.
 Check myexists I, I = 0. (* Should not be seen as a constructor *)
 End M14.
+
+(* 15. Testing different ways to give the same levels without failing *)
+
+Module M15.
+  Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level).
+  Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
+  Local Notation "###### x" := (S x) (at level 79).
+End M15.
+
+(* 16. Some test about custom entries *)
+Module M16.
+  (* Test locality *)
+  Local Declare Custom Entry foo.
+  Fail Notation "#" := 0 (in custom foo). (* Should be local *)
+  Local Notation "#" := 0 (in custom foo).
+
+  (* Test import *)
+  Module A.
+  Declare Custom Entry foo2.
+  End A.
+  Fail Notation "##" := 0 (in custom foo2).
+  Import A.
+  Local Notation "##" := 0 (in custom foo2).
+
+  (* Test Print Grammar *)
+  Print Grammar foo.
+  Print Grammar foo2.
+End M16.
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
new file mode 100644
index 0000000000..83fb3d0c8e
--- /dev/null
+++ b/test-suite/success/attribute-syntax.v
@@ -0,0 +1,23 @@
+From Coq Require Program.
+
+Section Scope.
+
+#[local] Coercion nat_of_bool (b: bool) : nat :=
+  if b then 0 else 1.
+
+Check (refl_equal : true = 0 :> nat).
+
+End Scope.
+
+Fail Check 0 = true :> nat.
+
+#[polymorphic]
+Definition ι T (x: T) := x.
+
+Check ι _ ι.
+
+#[program]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+
+#[deprecated(since="8.9.0")]
+Ltac foo := foo.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 7ca2767a53..299b08bdd1 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -193,12 +193,13 @@ Set Primitive Projections.
 Record s (x:nat) (y:=S x) := {c:=x; d:x=c}.
 Lemma f : 0=1.
 Proof.
-Fail apply d.
+  Fail apply d.
 (*
 split.
 reflexivity.
 Qed.
 *)
+Abort.
 
 (* Primitive projection match compilation *)
 Require Import List.
@@ -220,3 +221,9 @@ Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) :=
 Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *)
 Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *)
 Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *)
+
+Check (@eq_refl _ 0 <: 0 = fst (pair 0 1)).
+Fail Check (@eq_refl _ 0 <: 0 = snd (pair 0 1)).
+
+Check (@eq_refl _ 0 <<: 0 = fst (pair 0 1)).
+Fail Check (@eq_refl _ 0 <<: 0 = snd (pair 0 1)).
diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/success/ssr_delayed_clear_rename.v
deleted file mode 100644
index 951e5aff79..0000000000
--- a/test-suite/success/ssr_delayed_clear_rename.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Import ssreflect.
-Example foo (t t1 t2 : True) : True /\ True -> True -> True.
-Proof.
-move=>[{t1 t2 t} t1 t2] t.
-Abort.
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
new file mode 100644
index 0000000000..42236a5313
--- /dev/null
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -0,0 +1,13 @@
+Set Uniform Inductive Parameters.
+
+Inductive list (A : Type) :=
+  | nil : list
+  | cons : A -> list -> list.
+Check (list : Type -> Type).
+Check (cons : forall A, A -> list A -> list A).
+
+Inductive list2 (A : Type) (A' := prod A A) :=
+  | nil2 : list2
+  | cons2 : A' -> list2 -> list2.
+Check (list2 : Type -> Type).
+Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).