- Force every universe level to be >= Prop, so one cannot "go under" it anymore.

- Finish the change to level-to-level substitutions, in the checker.

6 files changed, 14 insertions, 13 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index d650e194e..d23740ca7 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -125,7 +125,7 @@ let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
       let subst, csts = universes_and_subst_of cb u in
-	(map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
+	(map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
 exception NotEvaluableConst of const_evaluation_result
@@ -137,7 +137,7 @@ let constant_value env (kn,u) =
       let b = force_constr l_body in
 	if cb.const_polymorphic then
 	  let subst = Univ.make_universe_subst u cb.const_universes in
-	    subst_univs_constr subst b
+	    subst_univs_level_constr subst b
 	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 55acd9f97..29eca3d82 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -57,11 +57,11 @@ let inductive_params (mib,_) = mib.mind_nparams
 let make_inductive_subst mib u =
   if mib.mind_polymorphic then 
     make_universe_subst u mib.mind_universes
-  else Univ.empty_subst
+  else Univ.empty_level_subst
 
 let inductive_params_ctxt (mib,u) = 
   let subst = make_inductive_subst mib u in
-    subst_univs_context subst mib.mind_params_ctxt
+    subst_univs_level_context subst mib.mind_params_ctxt
 
 let inductive_instance mib =
   if mib.mind_polymorphic then 
@@ -90,7 +90,7 @@ let ind_subst mind mib u =
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind u subst mib c =
   let s = ind_subst mind mib u in
-  substl s (subst_univs_constr subst c)
+  substl s (subst_univs_level_constr subst c)
 
 let instantiate_params full t args sign =
   let fail () =
@@ -114,7 +114,7 @@ let full_inductive_instantiate mib u params sign =
   let t = mkArity (sign,dummy) in
   let subst = make_inductive_subst mib u in
   let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    subst_univs_context subst ar
+    subst_univs_level_context subst ar
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
   let subst = make_inductive_subst mib u in
@@ -231,7 +231,7 @@ let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
     if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
     else 
       let subst = make_inductive_subst mib u in
-	(subst_univs_constr subst a.mind_user_arity, subst)
+	(subst_univs_level_constr subst a.mind_user_arity, subst)
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -248,7 +248,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
     if not mib.mind_polymorphic then a.mind_user_arity
     else 
       let subst = make_inductive_subst mib u in
-	(subst_univs_constr subst a.mind_user_arity)
+	(subst_univs_level_constr subst a.mind_user_arity)
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index e223af0c9..dfdda3179 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -22,7 +22,8 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> Univ.universe_subst
+val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> 
+  Univ.universe_level_subst
 val inductive_instance : mutual_inductive_body -> Univ.universe_instance
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
diff --git a/checker/term.ml b/checker/term.ml
index ad26c5edc..0f8aa804f 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -478,5 +478,5 @@ let subst_univs_level_constr subst c =
     let c' = aux c in
       if !changed then c' else c
 
-let subst_univs_context s = 
-  map_rel_context (subst_univs_constr s)
+let subst_univs_level_context s = 
+  map_rel_context (subst_univs_level_constr s)
diff --git a/checker/term.mli b/checker/term.mli
index cf488f536..5e98885fa 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -55,4 +55,4 @@ val eq_constr : constr -> constr -> bool
 
 val subst_univs_constr : Univ.universe_subst -> constr -> constr
 val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
-val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 887d9dc1d..a0640a55f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -226,7 +226,7 @@ let judge_of_projection env p c ct =
   in
     assert(eq_mind pb.proj_ind (fst ind));
     let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = subst_univs_constr usubst pb.proj_type in
+    let ty = subst_univs_level_constr usubst pb.proj_type in
       substl (c :: List.rev args) ty
 
 (* Fixpoints. *)