diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index da393b2354..549496d918 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -40,6 +40,18 @@ type local_entry = (* Inductive entries *) +type elimination_sorts = ElimOnProp | ElimOnSet | ElimOnType + +let sort_of_elimination = function + | ElimOnProp -> prop + | ElimOnSet -> spec + | ElimOnType -> Type (Univ.new_univ ()) + +let elimination_of_sort = function + | Prop Null -> ElimOnProp + | Prop Pos -> ElimOnSet + | Type _ -> ElimOnType + type recarg = | Param of int | Norec @@ -56,7 +68,7 @@ type one_inductive_body = { mind_user_arity : types option; mind_sort : sorts; mind_nrealargs : int; - mind_kelim : sorts list; + mind_kelim : elimination_sorts list; mind_listrec : (recarg list) array; mind_finite : bool; mind_nparams : int; |