From aa09258de6757dd38328975de2f6de7991807c68 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Sep 2001 12:28:43 +0000
Subject: 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
---
 kernel/declarations.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

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;
-- 
cgit v1.2.3