aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_13303.v27
-rw-r--r--test-suite/bugs/closed/bug_13456.v5
-rw-r--r--test-suite/misc/quotation_token/src/quotation.mlg2
-rw-r--r--test-suite/misc/side-eff-leak-univs/src/evil.mlg4
-rw-r--r--test-suite/output/UnivBinders.out143
-rw-r--r--test-suite/output/UnivBinders.v62
-rw-r--r--test-suite/output/ssr_pred.out3
-rw-r--r--test-suite/output/ssr_pred.v3
-rw-r--r--test-suite/success/CompatCurrentFlag.v4
-rw-r--r--test-suite/success/CompatOldFlag.v4
-rw-r--r--test-suite/success/CompatOldOldFlag.v6
-rw-r--r--test-suite/success/CompatPreviousFlag.v4
-rw-r--r--test-suite/success/evars.v9
-rw-r--r--test-suite/success/typing_flags.v47
-rwxr-xr-xtest-suite/tools/update-compat/run.sh2
15 files changed, 219 insertions, 106 deletions
diff --git a/test-suite/bugs/closed/bug_13303.v b/test-suite/bugs/closed/bug_13303.v
new file mode 100644
index 0000000000..6bee24b48a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13303.v
@@ -0,0 +1,27 @@
+Module Pt1.
+
+ Module M. Universe i. End M.
+ Module N. Universe i. End N.
+ Import M.
+ Notation foo := Type@{i (* M.i??? *)}.
+ Import N.
+ Fail Check foo : Type@{M.i}. (* should NOT succeed *)
+ Check foo : Type@{i (* N.i *)}. (* should succeed *)
+
+ Definition bar@{i} := Type@{i}.
+ Check bar : Type@{N.i}.
+ Check bar : Type@{M.i}.
+
+End Pt1.
+
+Module Pt2.
+
+ Module M. Universe i. Notation foo := Type@{i}. End M.
+
+ Definition foo1 := M.foo.
+ (* should succeed, currently errors undeclared universe i *)
+
+ Definition foo2@{i} : Type@{i} := M.foo.
+ (* should succeed, currently errors universe inconsistency *)
+
+End Pt2.
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/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
index ba0bcb1b3c..0f843b3b14 100644
--- a/test-suite/misc/quotation_token/src/quotation.mlg
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram
term: LEVEL "0"
[ [ s = QUOTATION "foobar:" ->
{
- CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
+ CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ]
;
END
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
index d89ab887a8..bb6eaff409 100644
--- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg
+++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
@@ -7,7 +7,7 @@ open Stdarg
TACTIC EXTEND magic
| [ "magic" ident(i) ident(j) ] -> {
- let open Glob_term in
- DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
+ let open Constrexpr in
+ DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
}
END
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d8d3f696b7..0fbb4f4c11 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,61 +1,61 @@
-Inductive Empty@{u} : Type@{u} :=
-(* u |= *)
-Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
-(* u |= *)
+Inductive Empty@{uu} : Type@{uu} :=
+(* uu |= *)
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+(* uu |= *)
PWrap has primitive projections with eta conversion.
Arguments PWrap _%type_scope
Arguments pwrap _%type_scope _
-punwrap@{u} =
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
- : forall A : Type@{u}, PWrap@{u} A -> A
-(* u |= *)
+punwrap@{uu} =
+fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
+ : forall A : Type@{uu}, PWrap@{uu} A -> A
+(* uu |= *)
Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
-(* u |= *)
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+(* uu |= *)
Arguments RWrap _%type_scope
Arguments rwrap _%type_scope _
-runwrap@{u} =
-fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
- : forall A : Type@{u}, RWrap@{u} A -> A
-(* u |= *)
+runwrap@{uu} =
+fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
+ : forall A : Type@{uu}, RWrap@{uu} A -> A
+(* uu |= *)
Arguments runwrap _%type_scope _
-Wrap@{u} = fun A : Type@{u} => A
- : Type@{u} -> Type@{u}
-(* u |= *)
+Wrap@{uu} = fun A : Type@{uu} => A
+ : Type@{uu} -> Type@{uu}
+(* uu |= *)
Arguments Wrap _%type_scope
-wrap@{u} =
-fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
- : forall A : Type@{u}, Wrap@{u} A -> A
-(* u |= *)
+wrap@{uu} =
+fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
+ : forall A : Type@{uu}, Wrap@{uu} A -> A
+(* uu |= *)
Arguments wrap {A}%type_scope {Wrap}
-bar@{u} = nat
- : Wrap@{u} Set
-(* u |= Set < u *)
-foo@{u u0 v} =
-Type@{u0} -> Type@{v} -> Type@{u}
- : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |= *)
+bar@{uu} = nat
+ : Wrap@{uu} Set
+(* uu |= Set < uu *)
+foo@{uu u v} =
+Type@{u} -> Type@{v} -> Type@{uu}
+ : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |= *)
Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
= Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
-mono = Type@{mono.u}
- : Type@{mono.u+1}
-(* {mono.u} |= *)
+mono = Type@{mono.uu}
+ : Type@{mono.uu+1}
+(* {mono.uu} |= *)
mono
- : Type@{mono.u+1}
-Type@{mono.u}
- : Type@{mono.u+1}
+ : Type@{mono.uu+1}
+Type@{mono.uu}
+ : Type@{mono.uu+1}
The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
monomono
: Type@{MONOU+1}
mono.monomono
@@ -63,23 +63,23 @@ mono.monomono
monomono
: Type@{MONOU+1}
mono
- : Type@{mono.u+1}
+ : Type@{mono.uu+1}
The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
bobmorane =
let tt := Type@{UnivBinders.32} in
let ff := Type@{UnivBinders.34} in tt -> ff
: Type@{max(UnivBinders.31,UnivBinders.33)}
The command has indeed failed with message:
-Universe u already bound.
+Universe uu already bound.
foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
: Type@{max(E+1,M+1,N+1)}
(* E M N |= *)
-foo@{u u0 v} =
-Type@{u0} -> Type@{v} -> Type@{u}
- : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |= *)
+foo@{uu u v} =
+Type@{u} -> Type@{v} -> Type@{uu}
+ : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |= *)
Inductive Empty@{E} : Type@{E} :=
(* E |= *)
Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -103,45 +103,38 @@ The command has indeed failed with message:
This object does not support universe names.
The command has indeed failed with message:
Cannot enforce v < u because u < gU < gV < v
-bind_univs.mono =
-Type@{bind_univs.mono.u}
- : Type@{bind_univs.mono.u+1}
-(* {bind_univs.mono.u} |= *)
-bind_univs.poly@{u} = Type@{u}
- : Type@{u+1}
-(* u |= *)
-insec@{v} = Type@{u} -> Type@{v}
- : Type@{max(u+1,v+1)}
+insec@{v} = Type@{uu} -> Type@{v}
+ : Type@{max(uu+1,v+1)}
(* v |= *)
Inductive insecind@{k} : Type@{k+1} :=
inseccstr : Type@{k} -> insecind@{k}
(* k |= *)
Arguments inseccstr _%type_scope
-insec@{u v} = Type@{u} -> Type@{v}
- : Type@{max(u+1,v+1)}
-(* u v |= *)
-Inductive insecind@{u k} : Type@{k+1} :=
- inseccstr : Type@{k} -> insecind@{u k}
-(* u k |= *)
+insec@{uu v} = Type@{uu} -> Type@{v}
+ : Type@{max(uu+1,v+1)}
+(* uu v |= *)
+Inductive insecind@{uu k} : Type@{k+1} :=
+ inseccstr : Type@{k} -> insecind@{uu k}
+(* uu k |= *)
Arguments inseccstr _%type_scope
insec2@{u} = Prop
: Type@{Set+1}
(* u |= *)
-inmod@{u} = Type@{u}
- : Type@{u+1}
-(* u |= *)
-SomeMod.inmod@{u} = Type@{u}
- : Type@{u+1}
-(* u |= *)
-inmod@{u} = Type@{u}
- : Type@{u+1}
-(* u |= *)
-Applied.infunct@{u v} =
-inmod@{u} -> Type@{v}
- : Type@{max(u+1,v+1)}
-(* u v |= *)
+inmod@{uu} = Type@{uu}
+ : Type@{uu+1}
+(* uu |= *)
+SomeMod.inmod@{uu} = Type@{uu}
+ : Type@{uu+1}
+(* uu |= *)
+inmod@{uu} = Type@{uu}
+ : Type@{uu+1}
+(* uu |= *)
+Applied.infunct@{uu v} =
+inmod@{uu} -> Type@{v}
+ : Type@{max(uu+1,v+1)}
+(* uu v |= *)
axfoo@{i u u0} : Type@{u} -> Type@{i}
(* i u u0 |= *)
@@ -166,3 +159,13 @@ Arguments axbar' _%type_scope
Expands to: Constant UnivBinders.axbar'
The command has indeed failed with message:
When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
+foo@{i} = Type@{M.i} -> Type@{i}
+ : Type@{max(M.i+1,i+1)}
+(* i |= *)
+bind_univs.mono =
+Type@{bind_univs.mono.u}
+ : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |= *)
+bind_univs.poly@{u} = Type@{u}
+ : Type@{u+1}
+(* u |= *)
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 582a5e969a..ed6e90b2a6 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -5,32 +5,32 @@ Set Printing Universes.
(* Unset Strict Universe Declaration. *)
(* universe binders on inductive types and record projections *)
-Inductive Empty@{u} : Type@{u} := .
+Inductive Empty@{uu} : Type@{uu} := .
Print Empty.
Set Primitive Projections.
-Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }.
Print PWrap.
Print punwrap.
Unset Primitive Projections.
-Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Record RWrap@{uu} (A:Type@{uu}) := rwrap { runwrap : A }.
Print RWrap.
Print runwrap.
(* universe binders also go on the constants for operational typeclasses. *)
-Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Class Wrap@{uu} (A:Type@{uu}) := wrap : A.
Print Wrap.
Print wrap.
(* Instance in lemma mode used to ignore the binders. *)
-Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
+Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed.
Print bar.
Unset Strict Universe Declaration.
(* The universes in the binder come first, then the extra universes in
order of appearance. *)
-Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}.
Print foo.
Check Type@{i} -> Type@{j}.
@@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}.
Set Strict Universe Declaration.
(* Binders even work with monomorphic definitions! *)
-Monomorphic Definition mono@{u} := Type@{u}.
+Monomorphic Definition mono@{uu} := Type@{uu}.
Print mono.
Check mono.
-Check Type@{mono.u}.
+Check Type@{mono.uu}.
Module mono.
- Fail Monomorphic Universe u.
+ Fail Monomorphic Universe uu.
Monomorphic Universe MONOU.
Monomorphic Definition monomono := Type@{MONOU}.
@@ -60,28 +60,28 @@ Import mono.
Check monomono. (* unqualified MONOU *)
Check mono. (* still qualified mono.u *)
-Monomorphic Constraint Set < UnivBinders.mono.u.
+Monomorphic Constraint Set < UnivBinders.mono.uu.
Module mono2.
- Monomorphic Universe u.
+ Monomorphic Universe uu.
End mono2.
-Fail Monomorphic Definition mono2@{u} := Type@{u}.
+Fail Monomorphic Definition mono2@{uu} := Type@{uu}.
Module SecLet.
Unset Universe Polymorphism.
Section foo.
- (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+ (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
Unset Strict Universe Declaration.
- Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
- Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
+ Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *)
+ Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
Definition bobmorane := tt -> ff.
End foo.
Print bobmorane.
End SecLet.
(* fun x x => foo is nonsense with local binders *)
-Fail Definition fo@{u u} := Type@{u}.
+Fail Definition fo@{uu uu} := Type@{uu}.
(* Using local binders for printing. *)
Print foo@{E M N}.
@@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}.
Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
-(* Universe binders survive through compilation, sections and modules. *)
-Require TestSuite.bind_univs.
-Print bind_univs.mono.
-Print bind_univs.poly.
-
Section SomeSec.
- Universe u.
- Definition insec@{v} := Type@{u} -> Type@{v}.
+ Universe uu.
+ Definition insec@{v} := Type@{uu} -> Type@{v}.
Print insec.
Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
@@ -129,7 +124,7 @@ End SomeSec2.
Print insec2.
Module SomeMod.
- Definition inmod@{u} := Type@{u}.
+ Definition inmod@{uu} := Type@{uu}.
Print inmod.
End SomeMod.
Print SomeMod.inmod.
@@ -138,7 +133,7 @@ Print inmod.
Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
Module SomeFunct (In : SomeTyp).
- Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+ Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}.
End SomeFunct.
Module Applied := SomeFunct(SomeMod).
Print Applied.infunct.
@@ -147,7 +142,7 @@ Print Applied.infunct.
In polymorphic mode the domain Type gets separate universes for the
different axioms, but all axioms have to declare all universes. In
- polymorphic mode they get the same universes, ie the type is only
+ monomorphic mode they get the same universes, ie the type is only
interpd once. *)
Axiom axfoo@{i+} axbar : Type -> Type@{i}.
Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
@@ -155,3 +150,18 @@ Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
About axfoo. About axbar. About axfoo'. About axbar'.
Fail Axiom failfoo failbar@{i} : Type.
+
+(* Notation interaction *)
+Module Notas.
+ Unset Universe Polymorphism.
+ Module Import M. Universe i. End M.
+
+ Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
+ Print foo. (* must not print Type@{i} -> Type@{i} *)
+
+End Notas.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require TestSuite.bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
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/evars.v b/test-suite/success/evars.v
index 253b48e4d9..2308656f7c 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -426,3 +426,12 @@ Abort.
(* (reported as bug #7356) *)
Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
+
+(* A printing check in passing *)
+
+Axiom abs : forall T, T.
+Fail Type let x := _ in
+ ltac:(
+ let t := type of x in
+ unify x (abs t);
+ exact 0).
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 $?
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:28:45 +0000