From a9fe19e2fa8f2c8b9d06f2053e0f08cf52317705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Oct 2003 16:36:49 +0000
Subject: Message inductive large

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d009a668f8..ba7389915d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -152,7 +152,7 @@ let enforce_type_constructor env arsort smax cst =
   match smax, arsort with
     | Type uc, Type ua -> enforce_geq ua uc cst
     | Type uc, Prop Pos when engagement env <> Some StronglyConstructive ->
-        error "Large inductive types in Set need option -strongly-constructive"
+        error "Large inductive types must be in Type, unless option -strongly-constructive is set"
     | _,_ -> cst
 
 let type_one_constructor env_ar_par params arsort c =
-- 
cgit v1.2.3