9 files changed, 71 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v
new file mode 100644
index 0000000000..b2e7fa7be5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13456.v
@@ -0,0 +1,5 @@
+Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True.
+Proof.
+  exists _, pn.
+  exact I.
+Qed.
diff --git a/test-suite/output/ssr_pred.out b/test-suite/output/ssr_pred.out
new file mode 100644
index 0000000000..f00111ff97
--- /dev/null
+++ b/test-suite/output/ssr_pred.out
@@ -0,0 +1,3 @@
+in1W
+     : forall (T1 : predArgType) (D1 : {pred T1}) (P1 : T1 -> Prop),
+       (forall x : T1, P1 x) -> {in D1, forall x : T1, P1 x}
diff --git a/test-suite/output/ssr_pred.v b/test-suite/output/ssr_pred.v
new file mode 100644
index 0000000000..bd88af80a3
--- /dev/null
+++ b/test-suite/output/ssr_pred.v
@@ -0,0 +1,3 @@
+Require Import ssreflect ssrfun ssrbool.
+
+Check @in1W.
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 97b4e39168..f1dad301fd 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.13") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.14") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq813.
+Import Coq.Compat.Coq814.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index c06dd6e450..a737e0c98e 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
 Import Coq.Compat.Coq813.
 Import Coq.Compat.Coq812.
-Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..f4cf703ec7
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
+Import Coq.Compat.Coq813.
+Import Coq.Compat.Coq812.
+Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 83010f2149..07d5fcd3ab 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.13") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
 Import Coq.Compat.Coq813.
-Import Coq.Compat.Coq812.
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index bd20d9c804..4af2028e38 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -1,4 +1,51 @@
+From Coq Require Import Program.Tactics.
 
+(* Part using attributes *)
+
+#[bypass_check(guard)] Fixpoint att_f' (n : nat) : nat := att_f' n.
+#[bypass_check(guard)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n.
+
+#[bypass_check(universes)] Definition att_T := let t := Type in (t : t).
+#[bypass_check(universes)] Program Definition p_att_T := let t := Type in (t : t).
+
+#[bypass_check(positivity)]
+Inductive att_Cor :=
+| att_Over : att_Cor
+| att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor.
+
+Fail #[bypass_check(guard=no)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
+Fail #[bypass_check(universes=no)] Definition f_att_T := let t := Type in (t : t).
+
+Fail #[bypass_check(positivity=no)]
+Inductive f_att_Cor :=
+| f_att_Over : f_att_Cor
+| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor.
+
+Print Assumptions att_f'.
+Print Assumptions att_T.
+Print Assumptions att_Cor.
+
+(* Interactive + atts *)
+#[bypass_check(universes=yes)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
+#[bypass_check(universes=yes)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+#[bypass_check(universes=yes)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+
+(* Note: be aware of tactics invoking [Global.env()] if this test fails. *)
+#[bypass_check(guard=yes)] Fixpoint i_att_f' (n : nat) : nat.
+Proof. exact (i_att_f' n). Defined.
+
+#[bypass_check(guard=yes)] Fixpoint d_att_f' (n : nat) : nat.
+Proof. exact (d_att_f' n). Qed.
+
+(* check regular mode is still safe *)
+Fail Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
+Fail Definition f_att_T := let t := Type in (t : t).
+
+Fail Inductive f_att_Cor :=
+| f_att_Over : f_att_Cor
+| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor.
+
+(* Part using Set/Unset *)
 Print Typing Flags.
 Unset Guard Checking.
 Fixpoint f' (n : nat) : nat := f' n.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 7ff5571ffb..61273c4f37 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 --release || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?