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

6 files changed, 39 insertions, 15 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;
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;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 344ca87fbe..662692ecaa 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -101,11 +101,12 @@ let mind_check_wellformed env mie =
 
 let allowed_sorts issmall isunit = function
   | Type _ -> 
-      [prop;spec;types]
+      [ElimOnProp;ElimOnSet;ElimOnType]
   | Prop Pos -> 
-      if issmall then [prop;spec;types] else [prop;spec]
+      if issmall then [ElimOnProp;ElimOnSet;ElimOnType]
+      else [ElimOnProp;ElimOnSet]
   | Prop Null -> 
-      if isunit then [prop;spec] else [prop]
+      if isunit then [ElimOnProp;ElimOnSet] else [ElimOnProp]
 
 type ill_formed_ind =
   | LocalNonPos of int
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index cb6d7b1178..e42df6d9c5 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -41,7 +41,7 @@ val mis_ntypes : inductive_instance -> int
 val mis_nconstr : inductive_instance -> int
 val mis_nparams : inductive_instance -> int
 val mis_nrealargs : inductive_instance -> int
-val mis_kelim : inductive_instance -> sorts list
+val mis_kelim : inductive_instance -> elimination_sorts list
 val mis_recargs : inductive_instance -> (recarg list) array array
 val mis_recarg : inductive_instance -> (recarg list) array
 val mis_typename : inductive_instance -> identifier
diff --git a/kernel/term.mli b/kernel/term.mli
index 4c7d23cc4c..76daa96f0a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -152,7 +152,7 @@ val mkSet : constr
 val mkType : Univ.universe -> constr
 val prop : sorts
 val spec : sorts
-val types : sorts 
+(*val types : sorts *)
 val type_0 : sorts
 
 (* Construct an implicit (see implicit arguments in the RefMan).
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 10d0bb611a..317cc199d6 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,31 +301,37 @@ let is_correct_arity env sigma kelim (c,pj) indf t =
           srec (a2,a2') (Constraint.union u univ)
       | IsProd (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env sigma a2 in 
-          let ksort = (match kind_of_term k with IsSort s -> s 
-			 | _ -> raise (Arity None)) in
+          let ksort = match kind_of_term k with
+	    | IsSort s -> elimination_of_sort s 
+	    | _ -> raise (Arity None) in
 	  let ind = build_dependent_inductive indf in
           let univ =
             try conv env sigma a1 ind
             with NotConvertible -> raise (Arity None) in
-          if List.exists (base_sort_cmp CONV ksort) kelim then
+          if List.exists ((=) ksort) kelim then
 	    ((true,k), Constraint.union u univ)
           else 
 	    raise (Arity (Some(k,t',error_elim_expln env sigma k t')))
       | k, IsProd (_,_,_) ->
 	  raise (Arity None)
       | k, ki -> 
-	  let ksort = (match k with IsSort s -> s 
-                         | _ ->  raise (Arity None)) in
-          if List.exists (base_sort_cmp CONV ksort) kelim then 
+	  let ksort = match k with
+	    | IsSort s -> elimination_of_sort s
+            | _ ->  raise (Arity None) in
+          if List.exists ((=) ksort) kelim then 
 	    (false, pt'), u
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t')))
   in 
   try srec (pj.uj_type,t) Constraint.empty
   with Arity kinds ->
+    let create_sort = function 
+      | ElimOnProp -> prop
+      | ElimOnSet -> spec
+      | ElimOnType -> Type (Univ.new_univ ()) in
     let listarity =
-      (List.map (make_arity env true indf) kelim)
-      @(List.map (make_arity env false indf) kelim)
+      (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
+      @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)
     in 
     let ind = mis_inductive (fst (dest_ind_family indf)) in
     error_elim_arity CCI env ind listarity c pj kinds