diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 344ca87fb..662692eca 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -101,11 +101,12 @@ let mind_check_wellformed env mie = let allowed_sorts issmall isunit = function | Type _ -> - [prop;spec;types] + [ElimOnProp;ElimOnSet;ElimOnType] | Prop Pos -> - if issmall then [prop;spec;types] else [prop;spec] + if issmall then [ElimOnProp;ElimOnSet;ElimOnType] + else [ElimOnProp;ElimOnSet] | Prop Null -> - if isunit then [prop;spec] else [prop] + if isunit then [ElimOnProp;ElimOnSet] else [ElimOnProp] type ill_formed_ind = | LocalNonPos of int |