Correction du bug des types singletons pas sous-type de Set

(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).

Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).

Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 121 insertions, 98 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 305aa4e58..12ae25ca3 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -140,7 +140,7 @@ let small_unit constrsinfos =
 
 let extract_level (_,_,_,lc,lev) =
   (* Enforce that the level is not in Prop if more than two constructors *)
-  if Array.length lc >= 2 then sup base_univ lev else lev
+  if Array.length lc >= 2 then sup type0_univ lev else lev
 
 let inductive_levels arities inds =
   let levels = Array.map pi3 arities in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index c2301777d..febe312f2 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -127,8 +127,8 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> neutral_univ
-| Prop Pos -> base_univ
+| Prop Null -> lower_univ
+| Prop Pos -> type0_univ
 
 let cons_subst u su subst =
   try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
@@ -182,8 +182,8 @@ let instantiate_universes env ctx ar argsorts =
   let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
   let level = subst_large_constraints subst ar.poly_level in
   ctx,
-  if is_empty_univ level then Prop Null
-  else if is_base_univ level then Prop Pos
+  if is_lower_univ level then Prop Null
+  else if is_type0_univ level then Prop Pos
   else Type level
 
 let type_of_inductive_knowing_parameters env mip paramtyps =
@@ -204,11 +204,11 @@ let type_of_inductive env (_,mip) =
 
 let cumulate_constructor_univ u = function
   | Prop Null -> u
-  | Prop Pos -> sup base_univ u
+  | Prop Pos -> sup type0_univ u
   | Type u' -> sup u u'
 
 let max_inductive_sort =
-  Array.fold_left cumulate_constructor_univ neutral_univ
+  Array.fold_left cumulate_constructor_univ lower_univ
 
 (************************************************************************)
 (* Type of a constructor *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 5b289e0e1..27a3e287d 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -50,7 +50,7 @@ let assumption_of_judgment env j =
 
 (* Prop and Set *)
 
-let judge_of_prop = Sort (Type prop_univ)
+let judge_of_prop = Sort (Type type1_univ)
 
 (* Type of Type(i). *)
 
@@ -179,9 +179,9 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 base_univ)
+          Type (sup u1 type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup base_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index c9c0ed4b2..4ac4e9704 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -38,7 +38,7 @@ let add_sign (id,t) s =
 
 let cast_set c = mkCast (c, mkSet)
 
-let set = mkCast (mkSet, mkType Univ.prop_univ)
+let set = mkCast (mkSet, mkType Univ.type1_univ)
 
 (* [cci_sign_of env] construit un environnement pour CIC ne comprenant que
  * les objets fonctionnels de l'environnement de programes [env]
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 6ea000f5b..1a6cb9c81 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -263,7 +263,7 @@ let typeur sigma metamap =
        match sort_of env cstr with
           Coq_sort T.InProp -> T.mkProp
         | Coq_sort T.InSet -> T.mkSet
-        | Coq_sort T.InType -> T.mkType Univ.prop_univ (* ERROR HERE *)
+        | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *)
         | CProp -> T.mkConst DoubleTypeInference.cprop
                                                                                 
   and sort_of env t =
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ad7eaaf5e..7879b86f9 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -11,6 +11,20 @@ Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
 Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
 Eauto.simplest_apply -> Hiddentac.h_simplest_apply
 
+** Universe names (univ.mli)
+
+ base_univ -> type0_univ  (* alias of Set is the Type hierarchy *)
+ prop_univ -> type1_univ  (* the type of Set in the Type hierarchy *)
+ neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
+ is_base_univ -> is_type1_univ
+ is_empty_univ -> is_lower_univ
+
+** Sort names (term.mli)
+
+  mk_Set -> set_sort
+  mk_Prop -> prop_sort
+  type_0 -> type1_sort
+
 =========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
 =========================================
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c299ff553..764dfcc7b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -100,7 +100,7 @@ let mind_check_arities env mie =
 
 (* Typing the arities and constructor types *)
 
-let is_logic_type t = (t.utj_type = mk_Prop)
+let is_logic_type t = (t.utj_type = prop_sort)
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
    the product of a constructor or arity *)
@@ -157,7 +157,7 @@ let small_unit constrsinfos =
 
 let extract_level (_,_,_,lc,lev) =
   (* Enforce that the level is not in Prop if more than two constructors *)
-  if Array.length lc >= 2 then sup base_univ lev else lev
+  if Array.length lc >= 2 then sup type0_univ lev else lev
 
 let inductive_levels arities inds =
   let levels = Array.map pi3 arities in
@@ -262,7 +262,7 @@ let typecheck_inductive env mie =
 	  Inl (info,full_arity,s), enforce_geq u lev cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
 	  (* Predicative set: check that the content is indeed predicative *)
-	  if not (is_empty_univ lev) & not (is_base_univ lev) then
+	  if not (is_lower_univ lev) & not (is_type0_univ lev) then
 	    error "Large non-propositional inductive types must be in Type";
 	  Inl (info,full_arity,s), cst
       | Prop _ ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ac4efc515..2059a1a40 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -83,7 +83,7 @@ let instantiate_params full t args sign =
 let instantiate_partial_params = instantiate_params false
 
 let full_inductive_instantiate mib params sign =
-  let dummy = mk_Prop in
+  let dummy = prop_sort in
   let t = mkArity (sign,dummy) in
   fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
 
@@ -124,8 +124,8 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> neutral_univ
-| Prop Pos -> base_univ
+| Prop Null -> lower_univ
+| Prop Pos -> type0_univ
 
 let cons_subst u su subst =
   try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
@@ -179,9 +179,10 @@ let instantiate_universes env ctx ar argsorts =
   let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
   let level = subst_large_constraints subst ar.poly_level in
   ctx,
-  if is_empty_univ level then mk_Prop
-  else if is_base_univ level then mk_Set
-  else Type level
+  if is_type0_univ level then set_sort else Type level
+    (* Note: for singleton types, we keep a representative in Type so that
+       predicativity and subtyping in Set applies, even if the resulting type
+       is semantically equivalent to Prop (and indeed convertible to it) *)
 
 let type_of_inductive_knowing_parameters env mip paramtyps =
   match mip.mind_arity with
@@ -201,11 +202,11 @@ let type_of_inductive env (_,mip) =
 
 let cumulate_constructor_univ u = function
   | Prop Null -> u
-  | Prop Pos -> sup base_univ u
+  | Prop Pos -> sup type0_univ u
   | Type u' -> sup u u'
 
 let max_inductive_sort =
-  Array.fold_left cumulate_constructor_univ neutral_univ
+  Array.fold_left cumulate_constructor_univ lower_univ
 
 (************************************************************************)
 (* Type of a constructor *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ba7e8c41d..ee93ec291 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -151,6 +151,25 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
 
 (* Convertibility of sorts *)
 
+(* The sort cumulativity is
+
+    Prop, Set <= Type 1 <= ... <= Type i <= ...
+
+    and this holds whatever Set is predicative or impredicative
+
+    In addition, there are the following internal sorts:
+    - Type (-1) is semantically equivalent to Prop but with the
+      following syntactic restrictions: 
+      Type (-1) is syntactically predicative and subtype of all Type i
+      Prop is syntactically impredicative and subtype of Type i only for i>=1
+    - Type 0 is semantically equivalent to predicative Set
+    Both Type (-1) and Type 0 can only occur as types of polymorphic 
+    inductive types (in practice Type 0 is systematically converted to Set and
+    we do not see it outside the computation of polymorphic inductive but
+    Type (-1) is kept to avoid setting Prop <= predicative Set in the syntax;
+    this means that (*1*) below can happen).
+*)
+
 type conv_pb = 
   | CONV 
   | CUMUL
@@ -158,14 +177,13 @@ type conv_pb =
 let sort_cmp pb s0 s1 cuniv =
   match (s0,s1) with
     | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible
-    | (Prop c1, Type u)  ->
-        (match pb with
-            CUMUL -> cuniv
-          | _ -> raise NotConvertible)
+    | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
     | (Type u1, Type u2) ->
+	assert (is_univ_variable u2);
 	(match pb with
            | CONV -> enforce_eq u1 u2 cuniv
 	   | CUMUL -> enforce_geq u2 u1 cuniv)
+    | (Type u, Prop _) when u = lower_univ & pb = CUMUL -> cuniv    (*1*)
     | (_, _) -> raise NotConvertible
 
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0c31d7962..f5b3e87bd 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -112,7 +112,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
     let (ctx2,s2) = dest_arity env t2 in
     let s1,s2 =
       match s1, s2 with
-      | Type _, Type _ -> (* shortcut here *) mk_Prop, mk_Prop
+      | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
       | (Prop _, Type _) | (Type _,Prop _) -> error ()
       | _ -> (s1, s2) in
     check_conv cst conv_leq env 
@@ -222,13 +222,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
             | Type u when not (is_univ_variable u) ->
               (* Both types are inferred, no need to recheck them. We
                  cheat and collapse the types to Prop *)
-                Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop)
+                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
             | Prop _ ->
               (* The type in the interface is inferred, it may be the case
                  that the type in the implementation is smaller because
                  the body is more reduced. We safely collapse the upper
                  type to Prop *)
-                Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop)
+                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
             | Type _ ->
               (* The type in the interface is inferred and the type in the
                  implementation is not inferred or is inferred but from a
diff --git a/kernel/term.ml b/kernel/term.ml
index 45cd2fb0e..a15510158 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -43,8 +43,9 @@ type sorts =
   | Prop of contents                      (* proposition types *)
   | Type of universe
       
-let mk_Set  = Prop Pos
-let mk_Prop = Prop Null
+let prop_sort = Prop Null
+let set_sort = Prop Pos
+let type1_sort = Type type1_univ
 
 type sorts_family = InProp | InSet | InType
 
@@ -830,18 +831,14 @@ let mkMeta = mkMeta
 let mkVar = mkVar
 
 (* Construct a type *)
-let mkProp   = mkSort mk_Prop
-let mkSet    = mkSort mk_Set
+let mkProp   = mkSort prop_sort
+let mkSet    = mkSort set_sort
 let mkType u = mkSort (Type u)
 let mkSort   = function
   | Prop Null -> mkProp (* Easy sharing *)
   | Prop Pos -> mkSet
   | s -> mkSort s
 
-let prop = mk_Prop
-and spec = mk_Set
-and type_0 = Type prop_univ
-
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
 (* (that means t2 is declared as the type of t1) *)
 let mkCast = mkCast
diff --git a/kernel/term.mli b/kernel/term.mli
index 70c5ceded..9254a6ff8 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -21,9 +21,9 @@ type sorts =
   | Prop of contents       (* Prop and Set *)
   | Type of Univ.universe  (* Type *)
 
-val mk_Set  : sorts
-val mk_Prop : sorts
-val type_0  : sorts
+val set_sort  : sorts
+val prop_sort : sorts
+val type1_sort  : sorts
 
 (*s The sorts family of CCI. *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a09b0799b..616349ba0 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -59,11 +59,11 @@ let sort_judgment env j = (type_judgment env j).utj_type
 
 let judge_of_prop =
   { uj_val = mkProp;
-    uj_type = mkSort type_0 }
+    uj_type = mkSort type1_sort }
 
 let judge_of_set =
   { uj_val = mkSet;
-    uj_type = mkSort type_0 }
+    uj_type = mkSort type1_sort }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -237,9 +237,9 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 base_univ)
+          Type (sup u1 type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup base_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6e7fa4080..aa12f0a8b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -40,8 +40,8 @@ open Util
  *)
 
 type universe_level =
-  | Base
-  | Level of Names.dir_path * int
+  | PredicativeSet
+  | PredicativeLevel of Names.dir_path * int
 
 type universe =
   | Atom of universe_level
@@ -53,10 +53,10 @@ module UniverseOrdered = struct
 end
 
 let string_of_univ_level = function
-  | Base -> "0"
-  | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
+  | PredicativeSet -> "0"
+  | PredicativeLevel (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
-let make_univ (m,n) = Atom (Level (m,n))
+let make_univ (m,n) = Atom (PredicativeLevel (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
 
@@ -78,6 +78,8 @@ let pr_uni = function
 let super = function
   | Atom u -> 
       Max ([],[u])
+  | Max ([],[]) -> (* Used for polym. inductive types at the lower level *)
+      Max ([],[PredicativeSet])
   | Max _ ->
       anomaly ("Cannot take the successor of a non variable universe:\n"^
                "(maybe a bugged tactic)")
@@ -96,8 +98,6 @@ let sup u v =
 	let gtl'' = list_union gtl gtl' in
 	Max (list_subtract gel'' gtl'',gtl'')
 
-let neutral_univ = Max ([],[])
-
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
     { univ: universe_level; lt: universe_level list; le: universe_level list }
@@ -126,23 +126,32 @@ let declare_univ u g =
   else
     g
 
-(* The level of Set *)
-let base_univ = Atom Base
+(* The lower predicative level of the hierarchy that contains (impredicative)
+   Prop and singleton inductive types *)
+let lower_univ = Max ([],[])
+
+let is_lower_univ = function
+  | Max ([],[]) -> true
+  | _ -> false
+
+(* The level of predicative Set *)
+let type0_univ = Atom PredicativeSet
 
-let is_base_univ = function
-  | Atom Base -> true
-  | Max ([Base],[]) -> warning "Non canonical Set"; true
+let is_type0_univ = function
+  | Atom PredicativeSet -> true
+  | Max ([PredicativeSet],[]) -> warning "Non canonical Set"; true
   | u -> false
 
 let is_univ_variable = function
-  | Atom a when a<>Base -> true
+  | Atom a when a<>PredicativeSet -> true
   | _ -> false
 
 (* When typing [Prop] and [Set], there is no constraint on the level,
-   hence the definition of [prop_univ], the type of [Prop] *)
+   hence the definition of [type1_univ], the type of [Prop] *)
+
+let type1_univ = Max ([],[PredicativeSet])
 
 let initial_universes = UniverseMap.empty
-let prop_univ = Max ([],[Base])
 
 (* Every universe_level has a unique canonical arc representative *)
 
@@ -288,7 +297,7 @@ let check_eq g u v =
 let compare_greater g strict u v =
   let g = declare_univ u g in
   let g = declare_univ v g in
-  if not strict && compare_eq g v Base then true else
+  if not strict && compare_eq g v PredicativeSet then true else
   match compare g v u with
     | (EQ|LE) -> not strict
     | LT -> true
@@ -452,7 +461,7 @@ type constraint_function =
     universe -> universe -> constraints -> constraints
 
 let constraint_add_leq v u c =
-  if v = Base then c else Constraint.add (v,Leq,u) c
+  if v = PredicativeSet then c else Constraint.add (v,Leq,u) c
 
 let enforce_geq u v c =
   match u, v with
@@ -476,7 +485,7 @@ let merge_constraints c g =
 (* Temporary inductive type levels *)
 
 let fresh_level =
-  let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n)
+  let n = ref 0 in fun () -> incr n; PredicativeLevel (Names.make_dirpath [],!n)
 
 let fresh_local_univ () = Atom (fresh_level ())
 
@@ -491,10 +500,6 @@ let remove_large_constraint u = function
   | Atom u' as x -> if u = u' then Max ([],[]) else x
   | Max (le,lt) -> make_max (list_remove u le,lt)
 
-let is_empty_univ = function
-  | Max ([],[]) -> true
-  | _ -> false
-
 let is_direct_constraint u = function
   | Atom u' -> u = u'
   | Max (le,lt) -> List.mem u le
@@ -607,8 +612,8 @@ module Huniv =
       type t = universe
       type u = Names.dir_path -> Names.dir_path
       let hash_aux hdir = function
-	| Base -> Base
-	| Level (d,n) -> Level (hdir d,n)
+	| PredicativeSet -> PredicativeSet
+	| PredicativeLevel (d,n) -> PredicativeLevel (hdir d,n)
       let hash_sub hdir = function
 	| Atom u -> Atom (hash_aux hdir u)
 	| Max (gel,gtl) ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c6f100dab..ce25afb26 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,12 +12,13 @@
 
 type universe
 
-val base_univ : universe
-val prop_univ : universe
-val neutral_univ : universe
+val type0_univ : universe  (* predicative Set seen as a universe *)
+val type1_univ : universe  (* the universe of the type of Prop/Set *)
+val lower_univ : universe  (* image of Prop in the predicative hierarchy *)
 val make_univ : Names.dir_path * int -> universe
 
-val is_base_univ : universe -> bool
+val is_type0_univ : universe -> bool
+val is_lower_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
 (* The type of a universe *)
@@ -66,8 +67,6 @@ val fresh_local_univ : unit -> universe
 val solve_constraints_system : universe option array -> universe array -> 
   universe array
 
-val is_empty_univ : universe -> bool
-
 val subst_large_constraint : universe -> universe -> universe -> universe
 
 val subst_large_constraints : 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e825b3f48..d7573b534 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -611,25 +611,14 @@ let pb_equal = function
   | CUMUL -> CONV
   | CONV -> CONV
 
-let sort_cmp pb s0 s1 cuniv =
-  match (s0,s1) with
-    | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible
-    | (Prop c1, Type u)  ->
-        (match pb with
-            CUMUL -> cuniv
-          | _ -> raise NotConvertible)
-    | (Type u1, Type u2) ->
-	(match pb with
-           | CONV -> enforce_eq u1 u2 cuniv
-	   | CUMUL -> enforce_geq u2 u1 cuniv)
-    | (_, _) -> raise NotConvertible
+let sort_cmp = sort_cmp
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
     | (Prop c1, Prop c2) -> c1 = c2
     | (Prop c1, Type u)  -> pb = CUMUL
     | (Type u1, Type u2) -> true
-    | (_, _) -> false
+    | (Type u, Prop _) -> u = lower_univ & pb = CUMUL
 
 
 let test_conversion f env sigma x y =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 635a579c0..795627fc4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -84,7 +84,7 @@ let retype sigma metamap =
   and sort_of env t = 
     match kind_of_term t with
     | Cast (c,_, s) when isSort s -> destSort s
-    | Sort (Prop c) -> type_0
+    | Sort (Prop c) -> type1_sort
     | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
         (match (sort_of env t, sort_of (push_rel (name,None,t) env) c2) with
@@ -92,8 +92,8 @@ let retype sigma metamap =
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when
               Environ.engagement env = Some ImpredicativeSet -> s
-          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.base_univ)
-	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
+          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
+	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
     | App(f,args) when isGlobalRef f ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 01104a815..a81f68b79 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -163,15 +163,15 @@ let new_Type_sort () = Type (new_univ ())
 let refresh_universes t =
   let modified = ref false in
   let rec refresh t = match kind_of_term t with
-    | Sort (Type _) -> modified := true; new_Type ()
+    | Sort (Type u) when u <> Univ.lower_univ -> modified := true; new_Type ()
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
     | _ -> t in
   let t' = refresh t in
   if !modified then t' else t
 
 let new_sort_in_family = function 
-  | InProp -> mk_Prop
-  | InSet -> mk_Set
+  | InProp -> prop_sort
+  | InSet -> set_sort
   | InType -> Type (new_univ ())
 
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index dd0fecc82..dd716024d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -234,10 +234,10 @@ open Leminv
 
 VERNAC COMMAND EXTEND DeriveInversionClear
   [ "Derive" "Inversion_clear" ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ]
+  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_clear_tac ]
+  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
@@ -257,10 +257,10 @@ VERNAC COMMAND EXTEND DeriveInversion
   -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_tac ]
+  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
 
 | [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_tac ]
+  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion