From aae1ebe54ab2ea42111e4c429d96129ce176acf5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 Dec 2003 11:47:27 +0000
Subject: Pour eviter d'avoir un gros type dans Set

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5071 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/inds_type_sec.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 2159c36b60..25a9976d96 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -6,5 +6,5 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 Section S.
-Inductive T [U:Type] : Set := c : U -> (T U).
+Inductive T [U:Type] : Type := c : U -> (T U).
 End S.
-- 
cgit v1.2.3