Actually exporting delayed universes in the EConstr implementation.

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

12 files changed, 56 insertions, 31 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8794f238bc..542db7fdfa 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 cad21543ba..30b83cf884 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 1adda14abe..84022f57f2 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 85cc8762ee..b6fa257691 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 20d86f81b6..c5ae684e3b 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 4d78d2eb0f..77086d046c 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 d5967c4bfc..88c492f03d 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 846d8055aa..c673851c84 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 18416b1424..01707b47a7 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 bb1b2901e5..9c9751af81 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 dec22ecd00..d9d64e7eb3 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 611d165fe1..035b0c2230 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