4 files changed, 32 insertions, 28 deletions
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index b8cae47196..e6d674c1e6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -29,3 +29,25 @@ Canonical Structure bool_test := mk_test (fun x y => x || y).
 Definition b := bool.
 
 Check (fun x : b => x != x).
+
+Inductive four := x0 | x1 | x2 | x3.
+Structure local := MKL { l : four }.
+
+Section X.
+  Definition s0 := MKL x0.
+  #[local] Canonical Structure s0.
+  Check (refl_equal _ : l _ = x0).
+
+  #[local] Canonical Structure s1 := MKL x1.
+  Check (refl_equal _ : l _ = x1).
+
+  Local Canonical Structure s2 := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+
+End X.
+Fail Check (refl_equal _ : l _ = x0).
+Fail Check (refl_equal _ : l _ = x1).
+Fail Check (refl_equal _ : l _ = x2).
+Check s0.
+Check s1.
+Check s2.
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index 96814a1b97..60d40d3d12 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -3,19 +3,11 @@ Module Syndefs.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation zar := Prop (compat "8.9").
-
 Check foo.
-Check bar.
 
 Set Warnings "+deprecated".
 
 Fail Check foo.
-Fail Check bar.
 
 End Syndefs.
 
@@ -24,19 +16,11 @@ Module Notations.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation "**" := Prop (compat "8.9").
-
 Check !!.
-Check ##.
 
 Set Warnings "+deprecated".
 
 Fail Check !!.
-Fail Check ##.
 
 End Notations.
 
@@ -45,18 +29,10 @@ Module Infix.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.9").
-
 Check (_ !! _).
-Check (_ ## _).
 
 Set Warnings "+deprecated".
 
 Fail Check (_ !! _).
-Fail Check (_ ## _).
 
 End Infix.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 6370cab6b2..4fac798f76 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1210,7 +1210,3 @@ Proof.
  constructor.
  trivial.
 Qed.
-
-
-
-
diff --git a/test-suite/success/cofixtac.v b/test-suite/success/cofixtac.v
new file mode 100644
index 0000000000..ae75ee770f
--- /dev/null
+++ b/test-suite/success/cofixtac.v
@@ -0,0 +1,10 @@
+CoInductive stream :=
+| C : content -> stream
+with content :=
+| D : nat -> stream -> content.
+
+Lemma one : stream.
+cofix c with (d : content).
+- constructor. apply d.
+- constructor. exact 1. apply c.
+Defined.