From bac707973955ef64eadae24ea01e029a5394626e Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 28 Oct 2003 14:44:33 +0000 Subject: Set devient predicatif par defaut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/indtypes.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5a1864316..d009a668f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -148,9 +148,11 @@ let small_unit constrsinfos = (* [smax] is the max of the sorts of the products of the constructor type *) -let enforce_type_constructor arsort smax cst = +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" | _,_ -> cst let type_one_constructor env_ar_par params arsort c = @@ -163,7 +165,7 @@ let type_one_constructor env_ar_par params arsort c = (* If the arity is at some level Type arsort, then the sort of the constructor must be below arsort; here we consider constructors with the global parameters (which add a priori more constraints on their sort) *) - let cst2 = enforce_type_constructor arsort j.utj_type cst in + let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in (infos, full_cstr_type, cst2) -- cgit v1.2.3