diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-10 12:28:43 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-10 12:28:43 +0000 |
commit | aa09258de6757dd38328975de2f6de7991807c68 (patch) | |
tree | dcf3658867f43845e3bb42a8a968d351ac695a86 /kernel/declarations.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/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 da393b235..549496d91 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; |