diff options
| author | herbelin | 2001-09-10 12:28:43 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-10 12:28:43 +0000 |
| commit | aa09258de6757dd38328975de2f6de7991807c68 (patch) | |
| tree | dcf3658867f43845e3bb42a8a968d351ac695a86 /kernel/indtypes.ml | |
| parent | fa621d5f5757d26ee7d47b145a9f3bab97cae655 (diff) | |
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les éliminations, pour éviter les collisions avec les univers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
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 344ca87fbe..662692ecaa 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 |