Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.

21 files changed, 140 insertions, 54 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 094841d69..166340b41 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -16,12 +16,19 @@ open Evd
 
 module API :
 sig
+module ESorts :
+sig
+type t
+val make : Sorts.t -> t
+val kind : Evd.evar_map -> t -> Sorts.t
+val unsafe_to_sorts : t -> Sorts.t
+end
 type t
-val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
@@ -33,6 +40,16 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t)
 end =
 struct
 
+module ESorts =
+struct
+  type t = Sorts.t
+  let make s = s
+  let kind sigma = function
+  | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+  | s -> s
+  let unsafe_to_sorts s = s
+end
+
 type t = Constr.t
 
 let safe_evar_value sigma ev =
@@ -46,9 +63,6 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | Sort (Type u) ->
-    let u' = Evd.normalize_universe sigma u in
-    if u' == u then c else mkSort (Sorts.sort_of_univ u')
   | Const (c', u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
     if u' == u then c else mkConstU (c', u')
@@ -82,8 +96,25 @@ let of_constr c = c
 let unsafe_to_constr c = c
 let unsafe_eq = Refl
 
-let rec to_constr sigma t =
-  Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t)
+let rec to_constr sigma c = match Constr.kind c with
+| Evar ev ->
+  begin match safe_evar_value sigma ev with
+  | Some c -> to_constr sigma c
+  | None -> Constr.map (fun c -> to_constr sigma c) c
+  end
+| Sort (Type u) ->
+  let u' = Evd.normalize_universe sigma u in
+  if u' == u then c else mkSort (Sorts.sort_of_univ u')
+| Const (c', u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkConstU (c', u')
+| Ind (i, u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkIndU (i, u')
+| Construct (co, u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkConstructU (co, u')
+| _ -> Constr.map (fun c -> to_constr sigma c) c
 
 let of_named_decl d = d
 let unsafe_to_named_decl d = d
@@ -108,14 +139,14 @@ type rel_context = (constr, types) Context.Rel.pt
 
 let in_punivs a = (a, Univ.Instance.empty)
 
-let mkProp = of_kind (Sort Sorts.prop)
-let mkSet = of_kind (Sort Sorts.set)
-let mkType u = of_kind (Sort (Sorts.Type u))
+let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
+let mkSet = of_kind (Sort (ESorts.make Sorts.set))
+let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u)))
 let mkRel n = of_kind (Rel n)
 let mkVar id = of_kind (Var id)
 let mkMeta n = of_kind (Meta n)
 let mkEvar e = of_kind (Evar e)
-let mkSort s = of_kind (Sort s)
+let mkSort s = of_kind (Sort (ESorts.make s))
 let mkCast (b, k, t) = of_kind (Cast (b, k, t))
 let mkProd (na, t, u) = of_kind (Prod (na, t, u))
 let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
@@ -730,6 +761,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 
 module Unsafe =
 struct
+let to_sorts = ESorts.unsafe_to_sorts
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e7287fc06..db10fbf42 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -28,9 +28,26 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
+(** {5 Universe variables} *)
+
+module ESorts :
+sig
+  type t
+  (** Type of sorts up-to universe unification. Essentially a wrapper around
+      Sorts.t so that normalization is ensured statically. *)
+
+  val make : Sorts.t -> t
+  (** Turn a sort into an up-to sort. *)
+
+  val kind : Evd.evar_map -> t -> Sorts.t
+  (** Returns the view into the current sort. Note that the kind of a variable
+      may change if the unification state of the evar map changes. *)
+
+end
+
 (** {5 Destructors} *)
 
-val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
 (** Same as {!Constr.kind} except that it expands evars and normalizes
     universes on the fly. *)
 
@@ -43,7 +60,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
 
-val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 (** Construct a term from a view. *)
 
 val of_constr : Constr.t -> t
@@ -123,7 +140,7 @@ val isRelN : Evd.evar_map -> int -> t -> bool
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
 val destVar : Evd.evar_map -> t -> Id.t
-val destSort : Evd.evar_map -> t -> Sorts.t
+val destSort : Evd.evar_map -> t -> ESorts.t
 val destCast : Evd.evar_map -> t -> t * cast_kind * t
 val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
@@ -242,6 +259,9 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_sorts : ESorts.t -> Sorts.t
+  (** Physical identity. Does not care for normalization. *)
+
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
 end
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7b7302957..3b979f206 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -123,7 +123,7 @@ let hdchar env sigma c =
     | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
     | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
     | Var id  -> lowercase_first_char id
-    | Sort s -> sort_hdchar s
+    | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
diff --git a/engine/termops.ml b/engine/termops.ml
index 410fb75c5..a67916345 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1181,14 +1181,19 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
-  | Sort (Prop Null) -> true
+  | Sort u ->
+    begin match EConstr.ESorts.kind sigma u with
+    | Prop Null -> true
+    | _ -> false
+    end
   | Cast (c,_,_) -> is_Prop sigma c
   | _ -> false
 
 (* eq_constr extended with universe erasure *)
 let compare_constr_univ sigma f cv_pb t1 t2 =
+  let open EConstr in
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
-      Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+      Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
     | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 55172cba6..b84be4600 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -434,7 +434,7 @@ module TypeGlobal = struct
 end
 
 let sort_of_rel env evm rel =
-  Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
+  ESorts.kind evm (Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel))
 
 let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 114b8dda0..95620b374 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -164,7 +164,7 @@ let id_of_name = function
 	  basename
        | Sort s ->
 	  begin
-	    match s with
+	    match ESorts.kind sigma s with
 	    | Prop _ -> Label.to_id (Label.make "Prop")
 	    | Type _ -> Label.to_id (Label.make "Type")
 	  end
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index adf926958..a2016cb03 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1714,7 +1714,7 @@ let onClearedName2 id tac =
     end })
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
-  | Sort (Prop Null) -> true
+  | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
   | Cast (c,_,_) -> is_Prop sigma c
   | _ -> false
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8794f238b..542db7fdf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -199,7 +199,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
     in
       match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
       | Sort s, Sort s' ->
-        (match s, s' with
+        (match ESorts.kind !evdref s, ESorts.kind !evdref s' with
 	| Prop x, Prop y when x == y -> None
 	| Prop _, Type _ -> None
 	| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
@@ -406,7 +406,7 @@ let inh_app_fun resolve_tc env evd j =
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
-    | Sort s -> {utj_val = j.uj_val; utj_type = s }
+    | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s }
     | _ -> error_not_a_type env sigma j
 
 let inh_tosort_force loc env evd j =
@@ -421,7 +421,7 @@ let inh_tosort_force loc env evd j =
 let inh_coerce_to_sort loc env evd j =
   let typ = whd_all env evd j.uj_type in
     match EConstr.kind evd typ with
-    | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
+    | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s })
     | Evar ev ->
 	let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
 	  (evd',{ utj_val = j.uj_val; utj_type = s })
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index cad21543b..30b83cf88 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -205,11 +205,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 
       | PRel n1, Rel n2 when Int.equal n1 n2 -> subst
 
-      | PSort GProp, Sort (Prop Null) -> subst
-
-      | PSort GSet, Sort (Prop Pos) -> subst
-
-      | PSort (GType _), Sort (Type _) -> subst
+      | PSort ps, Sort s ->
+
+        begin match ps, ESorts.kind sigma s with
+        | GProp, Prop Null -> subst
+        | GSet, Prop Pos -> subst
+        | GType _, Type _ -> subst
+        | _ -> raise PatternMatchingFailure
+        end
 
       | PApp (p, [||]), _ -> sorec ctx env subst p t
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1adda14ab..84022f57f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -457,7 +457,7 @@ let rec detype flags avoid env sigma t =
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
-    | Sort s -> GSort (dl,detype_sort sigma s)
+    | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s))
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
         detype flags avoid env sigma c1
     | Cast (c1,k,c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 85cc8762e..b6fa25769 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -150,6 +150,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 	    (Stack.append_app [|a;pop b|] Stack.empty)
           else raise Not_found
       | Sort s ->
+        let s = ESorts.kind sigma s in
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
       | _ ->
@@ -775,6 +776,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
 	| Sort s1, Sort s2 when app_empty ->
 	    (try
+              let s1 = ESorts.kind evd s1 in
+              let s2 = ESorts.kind evd s2 in
 	       let evd' =
 		 if pbty == CONV
 		 then Evd.set_eq_sort env evd s1 s2
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 20d86f81b..c5ae684e3 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -91,7 +91,7 @@ let define_pure_evar_as_product evd evk =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
     let src = evar_source evk evd1 in
     let filter = Filter.extend 1 (evar_filter evi) in
-      if is_prop_sort s then
+      if is_prop_sort (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar_unsafe newenv evd1 concl ~src ~filter
       else
@@ -102,7 +102,7 @@ let define_pure_evar_as_product evd evk =
           (Sigma.to_evar_map evd3, e)
         in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
-	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
+	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in
 	  evd3, rng
   in
   let prod = mkProd (Name id, dom, subst_var id rng) in
@@ -174,7 +174,7 @@ let define_evar_as_sort env evd (ev,args) =
   let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
   let sort = destSort evd concl in
   let evd' = Evd.define ev (Constr.mkSort s) evd in
-  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
+  Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s
 
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4d78d2eb0..77086d046 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -50,6 +50,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   let modified = ref false in
   (* direction: true for fresh universes lower than the existing ones *)
   let refresh_sort status ~direction s =
+    let s = ESorts.kind !evdref s in
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
       if direction then set_leq_sort env !evdref s' s
@@ -59,7 +60,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let rec refresh ~onlyalg status ~direction t =
     match EConstr.kind !evdref t with
-    | Sort (Type u as s) ->
+    | Sort s ->
+      begin match ESorts.kind !evdref s with
+      | Type u ->
        (match Univ.universe_level u with
 	| None -> refresh_sort status ~direction s
 	| Some l ->
@@ -71,10 +74,12 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       if onlyalg && alg then
 	         (evdref := Evd.make_flexible_variable !evdref false l; t)
 	       else t))
-    | Sort (Prop Pos as s) when refreshset && not direction ->
+      | Prop Pos when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
           only refreshing when we want higher universes. *)
        refresh_sort status ~direction s
+      | _ -> t
+      end
     | Prod (na,u,v) -> 
       mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d5967c4bf..88c492f03 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -617,6 +617,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
     let _,scl = splay_arity env sigma conclty in
+    let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 846d8055a..c673851c8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1071,7 +1071,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
 and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
   | GHole (loc, knd, naming, None) ->
       let rec is_Type c = match EConstr.kind !evdref c with
-      | Sort (Type _) -> true
+      | Sort s ->
+        begin match ESorts.kind !evdref s with
+        | Type _ -> true
+        | Prop _ -> false
+        end
       | Cast (c, _, _) -> is_Type c
       | _ -> false
       in
@@ -1081,7 +1085,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	     let sigma =  !evdref in
 	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
 	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
-               | Sort s -> s
+               | Sort s -> ESorts.kind sigma s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 18416b142..01707b47a 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -215,8 +215,8 @@ val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
-val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
-val sort_of_arity : env -> evar_map -> constr -> sorts
+val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * ESorts.t
+val sort_of_arity : env -> evar_map -> constr -> ESorts.t
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
@@ -232,7 +232,7 @@ type 'a miota_args = {
 val reducible_mind_case : evar_map -> constr -> bool
 val reduce_mind_case : evar_map -> constr miota_args -> constr
 
-val find_conclusion : env -> evar_map -> constr -> (constr, constr, Sorts.t, Univ.Instance.t) kind_of_term
+val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bb1b2901e..9c9751af8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -77,7 +77,7 @@ let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
     match EConstr.kind sigma (whd_all env sigma ar), args with
     | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l
-    | Sort s, [] -> s
+    | Sort s, [] -> ESorts.kind sigma s
     | _ -> retype_error NotASort
   in concl_of_arity env 0 ft (Array.to_list args)
 
@@ -87,9 +87,11 @@ let type_of_var env id =
 
 let decomp_sort env sigma t =
   match EConstr.kind sigma (whd_all env sigma t) with
-  | Sort s -> s
+  | Sort s -> ESorts.kind sigma s
   | _ -> retype_error NotASort
 
+let destSort sigma s = ESorts.kind sigma (destSort sigma s)
+
 let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match EConstr.kind sigma cstr with
@@ -142,8 +144,11 @@ let retype ?(polyprop=true) sigma =
   and sort_of env t =
     match EConstr.kind sigma t with
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
-    | Sort (Prop c) -> type1_sort
-    | Sort (Type u) -> Type (Univ.super u)
+    | Sort s ->
+      begin match ESorts.kind sigma s with
+      | Prop _ -> type1_sort
+      | Type u -> Type (Univ.super u)
+      end
     | Prod (name,t,c2) ->
         (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
 	  | _, (Prop Null as s) -> s
@@ -163,8 +168,7 @@ let retype ?(polyprop=true) sigma =
   and sort_family_of env t =
     match EConstr.kind sigma t with
     | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s)
-    | Sort (Prop c) -> InType
-    | Sort (Type u) -> InType
+    | Sort _ -> InType
     | Prod (name,t,c2) ->
 	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dec22ecd0..d9d64e7eb 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -46,7 +46,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
 
 let e_type_judgment env evdref j =
   match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
-    | Sort s -> {utj_val = j.uj_val; utj_type = s }
+    | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
@@ -102,6 +102,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();
         srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
+        let s = ESorts.kind !evdref s in
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
     | Evar (ev,_), [] ->
@@ -161,7 +162,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
+  let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
@@ -288,11 +289,13 @@ let rec execute env evdref cstr =
         check_cofix env !evdref cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
-    | Sort (Prop c) ->
-	judge_of_prop_contents c
-
-    | Sort (Type u) ->
+    | Sort s ->
+      begin match ESorts.kind !evdref s with
+      | Prop c ->
+        judge_of_prop_contents c
+      | Type u ->
         judge_of_type u
+      end
 
     | Proj (p, c) -> 
         let cj = execute env evdref c in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 611d165fe..035b0c223 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -780,6 +780,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| Sort s1, Sort s2 ->
 	    (try 
+              let s1 = ESorts.kind sigma s1 in
+              let s2 = ESorts.kind sigma s2 in
 	       let sigma' = 
 		 if pb == CUMUL
 		 then Evd.set_leq_sort curenv sigma s1 s2 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c53e47d92..7eadde78d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -512,7 +512,11 @@ let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l)
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
   match EConstr.kind sigma ty with
-  | Sort (Prop Null) -> true
+  | Sort s ->
+    begin match ESorts.kind sigma s with
+    | Prop Null -> true
+    | _ -> false
+    end
   | _ -> false
 
 let is_unique env sigma concl =
diff --git a/vernac/command.ml b/vernac/command.ml
index 32b0abb8a..db203b425 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -987,8 +987,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       try
 	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
 	  match ctx, EConstr.kind !evdref ar with
-	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
-	      when Reductionops.is_conv env !evdref t u -> t
+	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort s
+	      when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t
 	  | _, _ -> error ()
       with e when CErrors.noncritical e -> error ()
   in