Merge PR #12586: [declare] Allow custom typing flags when declaring constants.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: jfehrle

1 files changed, 47 insertions, 0 deletions

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.