11 files changed, 92 insertions, 37 deletions
diff --git a/test-suite/bugs/closed/bug_10060.v b/test-suite/bugs/closed/bug_10060.v
new file mode 100644
index 0000000000..d74f6e388b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10060.v
@@ -0,0 +1,15 @@
+Module Type T.
+  Parameter b : Set.
+End T.
+
+Module M1(N : T).
+End M1.
+
+Module M2.
+End M2.
+
+Section S.
+  Variable a : Set.
+  Definition b := a.
+  Fail Include M1.
+End S.
diff --git a/test-suite/bugs/closed/bug_10903.v b/test-suite/bugs/closed/bug_10903.v
new file mode 100644
index 0000000000..3da63dfbb0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10903.v
@@ -0,0 +1,3 @@
+(* -*- coq-prog-args: ("-type-in-type"); -*- *)
+
+Inductive Ind : SProp := C : Ind -> Ind.
diff --git a/test-suite/bugs/closed/bug_11048.v b/test-suite/bugs/closed/bug_11048.v
new file mode 100644
index 0000000000..d1211587f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11048.v
@@ -0,0 +1,5 @@
+
+Inductive foo (HUGE := _) (b : HUGE) A :=
+  bar (X:match _ : HUGE as T return HUGE with T => match (A : T) -> True with _ => T end end)
+  : foo b A.
+(* uncaught destKO *)
diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v
new file mode 100644
index 0000000000..62c49e9ea7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8459.v
@@ -0,0 +1,24 @@
+Require Import Coq.Vectors.Vector.
+
+Axiom exfalso : False.
+
+Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
+(Vector.fold_left orb false l) = false ->
+(forall p, (Vector.nth l p  ) = false).
+Proof.
+intros.
+destruct l.
+inversion p.
+revert h l H.
+set (P := fun n p => forall (h : bool) (l : t bool n),
+fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
+revert n p.
+fix loop 1.
+unshelve eapply (@Fin.rectS P).
++ elim exfalso.
++ unfold P.
+  intros.
+  eapply all_then_someV.
+  exact H0.
+Fail Defined.
+Abort.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index c1b9a2b1c6..ba4ac5a8f9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -57,3 +57,5 @@ where
      |- Type] (pat, p0, p cannot be used)
 ?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
       |- Type] (pat, p0, p cannot be used)
+fun '{| |} => true
+     : R -> bool
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d1063bfd04..4b9d0abd95 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y.
 Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
 
 End K.
+
+Module EmptyRecordSyntax.
+
+Record R := { n : nat }.
+Check fun '{|n:=x|} => true.
+
+End EmptyRecordSyntax.
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v
deleted file mode 100644
index 1233a4b8f5..0000000000
--- a/test-suite/success/Compat88.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
-(** Check that various syntax usage is available without importing
-    relevant files. *)
-Require Coq.Strings.Ascii Coq.Strings.String.
-Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
-Require Coq.Reals.Rdefinitions.
-Require Coq.Numbers.Cyclic.Int63.Cyclic63.
-
-Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
-
-Check String.String "a" String.EmptyString.
-Check String.eqb "a" "a".
-Check Nat.eqb 1 1.
-Check BinNat.N.eqb 1 1.
-Check BinInt.Z.eqb 1 1.
-Check BinPos.Pos.eqb 1 1.
-Check Rdefinitions.Rplus 1 1.
-Check Int63.is_zero 1.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
deleted file mode 100644
index 20eef955b4..0000000000
--- a/test-suite/success/CompatOldOldFlag.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index d313ba0aa4..96814a1b97 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -1,13 +1,13 @@
 Module Syndefs.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.8").
+Notation bar := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation zar := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation zar := Prop (compat "8.9").
 
 Check foo.
 Check bar.
@@ -21,14 +21,14 @@ End Syndefs.
 
 Module Notations.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.8").
+Notation "##" := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation "**" := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation "**" := Prop (compat "8.9").
 
 Check !!.
 Check ##.
@@ -42,14 +42,14 @@ End Notations.
 
 Module Infix.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.8").
+Infix "##" := plus (at level 1, compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.9").
 
 Check (_ !! _).
 Check (_ ## _).
diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v
new file mode 100644
index 0000000000..f4d2f07db5
--- /dev/null
+++ b/test-suite/success/RefineInstance.v
@@ -0,0 +1,23 @@
+
+
+Class Foo := foo { a : nat; b : bool }.
+
+Fail Instance bla : Foo := { b:= true }.
+
+#[refine] Instance bla : Foo := { b:= true }.
+Proof.
+exact 0.
+Defined.
+
+Instance bli : Foo := { a:=1; b := false}.
+Check bli.
+
+Fail #[program, refine] Instance bla : Foo := {b := true}.
+
+#[program] Instance blo : Foo := {b := true}.
+Next Obligation. exact 2. Qed.
+Check blo.
+
+#[refine] Instance xbar : Foo := {a:=4; b:=true}.
+Proof. Qed.
+Check xbar.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 61273c4f37..7ff5571ffb 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
 # we assume that the script lives in test-suite/tools/update-compat/,
 # and that update-compat.py lives in dev/tools/
 cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --master || exit $?
+dev/tools/update-compat.py --assert-unchanged --release || exit $?