Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v
new file mode 100644
index 0000000000..f24d13b8af
--- /dev/null
+++ b/test-suite/success/CumulInd.v
@@ -0,0 +1,20 @@
+
+(* variances other than Invariant are forbidden for non-cumul inductives *)
+Fail Inductive foo@{+u} : Prop := .
+Fail Polymorphic Inductive foo@{*u} : Prop := .
+Inductive foo@{=u} : Prop := .
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+Inductive force_invariant@{=u} : Prop := .
+Fail Definition lift@{u v | u < v} (x:force_invariant@{u}) : force_invariant@{v} := x.
+
+Inductive force_covariant@{+u} : Prop := .
+Fail Definition lift@{u v | v < u} (x:force_covariant@{u}) : force_covariant@{v} := x.
+Definition lift@{u v | u < v} (x:force_covariant@{u}) : force_covariant@{v} := x.
+
+Fail Inductive not_irrelevant@{*u} : Prop := nirr (_ : Type@{u}).
+Inductive check_covariant@{+u} : Prop := cov (_ : Type@{u}).
+
+Fail Inductive not_covariant@{+u} : Prop := ncov (_ : Type@{u} -> nat).