diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 16:55:41 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 16:55:41 +0000 |
commit | f83572bc45b9ab6b72688eb22d125896541ccf16 (patch) | |
tree | 37e08a39ea53751d9fdd7dff4449f4125e3f7bfd /kernel/declarations.ml | |
parent | 3607bb83605ff596445e0f18016d1fbb3d66d584 (diff) |
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r-- | kernel/declarations.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 549496d91..28f26a3af 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -40,18 +40,6 @@ 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 @@ -68,7 +56,7 @@ type one_inductive_body = { mind_user_arity : types option; mind_sort : sorts; mind_nrealargs : int; - mind_kelim : elimination_sorts list; + mind_kelim : sorts_family list; mind_listrec : (recarg list) array; mind_finite : bool; mind_nparams : int; |