Merge PR #10291: Controlling typing flags with commands (no attribute)

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

1 files changed, 43 insertions, 0 deletions

diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
new file mode 100644
index 0000000000..bd20d9c804
--- /dev/null
+++ b/test-suite/success/typing_flags.v
@@ -0,0 +1,43 @@
+
+Print Typing Flags.
+Unset Guard Checking.
+Fixpoint f' (n : nat) : nat := f' n.
+
+Fixpoint f (n : nat) : nat.
+Proof.
+  exact (f n).
+Defined.
+
+Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end.
+
+Print Typing Flags.
+
+Set Guard Checking.
+
+Print Assumptions f.
+
+Unset Universe Checking.
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+Print Typing Flags.
+Set Universe Checking.
+
+Fail Definition g2 (n : nat) : T := T.
+
+Fail Definition e := fix e (n : nat) : nat := e n.
+
+Unset Positivity Checking.
+
+Inductive Cor :=
+| Over : Cor
+| Next : ((Cor -> list nat) -> list nat) -> Cor.
+
+Set Positivity Checking.
+Print Assumptions Cor.
+
+Inductive Box :=
+| box : forall n, f n = n -> g 2 -> Box.
+
+Print Assumptions Box.