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

1 files changed, 6 insertions, 1 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 18566a0c37..e9d83506ec 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -44,6 +44,11 @@ type local_entry =
 
 (*s Inductive types (internal representation). *)
 
+type elimination_sorts = ElimOnProp | ElimOnSet | ElimOnType
+
+val elimination_of_sort : sorts -> elimination_sorts
+val sort_of_elimination : elimination_sorts -> sorts
+
 type recarg = 
   | Param of int 
   | Norec 
@@ -65,7 +70,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;