Add a file for typing_flags in the test-suite.

1 files changed, 38 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..31550b45a6
--- /dev/null
+++ b/test-suite/success/typing_flags.v
@@ -0,0 +1,38 @@
+
+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 Universes Checking.
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+Print Typing Flags.
+Set Universes 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.