From bc2c1836ba4c878903288060bcb66a0ef1aaced6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 12 Feb 2020 14:05:53 +0100
Subject: Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)

---
 test-suite/success/uniform_inductive_parameters.v | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..651247937d 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,13 +1,23 @@
+Module Att.
+  #[uniform] Inductive list (A : Type) :=
+  | nil : list
+  | cons : A -> list -> list.
+  Check (list : Type -> Type).
+  Check (cons : forall A, A -> list A -> list A).
+End Att.
+
 Set Uniform Inductive Parameters.
 
 Inductive list (A : Type) :=
-  | nil : list
-  | cons : A -> list -> list.
+| nil : list
+| cons : A -> list -> list.
 Check (list : Type -> Type).
 Check (cons : forall A, A -> list A -> list A).
 
 Inductive list2 (A : Type) (A' := prod A A) :=
-  | nil2 : list2
-  | cons2 : A' -> list2 -> list2.
+| nil2 : list2
+| cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
+
+#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)).
-- 
cgit v1.2.3