diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-28 14:44:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-28 14:44:33 +0000 |
| commit | bac707973955ef64eadae24ea01e029a5394626e (patch) | |
| tree | 61021a18d8595fb0fb0ba3017ab51a1b0a119e68 /kernel/indtypes.ml | |
| parent | 7a9940d257b5cd95942df09dd8d16d3dd35b199c (diff) | |
Set devient predicatif par defaut
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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) |