From 4165cce72347466fbaa565247ae040a873b46694 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Feb 2020 10:53:10 +0100
Subject: Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive
 Parameters)"

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

(limited to 'test-suite')

diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 651247937d..42236a5313 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,23 +1,13 @@
-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