- 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.

11 files changed, 27 insertions, 36 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. *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 147efe86b..6c6095021 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1466,6 +1466,12 @@ let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty
 
 let is_initial_universes g = LMap.equal (==) g initial_universes
 
+let add_universe vlev g = 
+  let v = terminal vlev in
+  let proparc = prop_arc g in
+    enter_arc {proparc with le=vlev::proparc.le}
+      (enter_arc v g)
+      
 (* Constraints and sets of constraints. *)    
 
 type univ_constraint = Level.t * constraint_type * Level.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index bf04c62e2..9398e23ba 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -183,6 +183,8 @@ val initial_universes : universes
 
 val is_initial_universes : universes -> bool
 
+val add_universe : universe_level -> universes -> universes
+
 (** {6 Substitution} *)
 
 type universe_subst_fn = universe_level -> universe
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e8b360b86..038b91ec6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -436,9 +436,8 @@ let process_universe_constraints univs vars alg templ cstrs =
 		  instantiate_variable r' l vars
 		else if not (Univ.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
-		     one of them being Prop, disallow *)
-		  if Univ.Level.equal l' Univ.Level.prop || 
-		    Univ.Level.equal r' Univ.Level.prop then
+		     one of them being Prop/Set, disallow *)
+		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
 		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
 		  else
 		    if fo then 
@@ -1013,7 +1012,8 @@ let uctx_new_univ_variable template rigid name
     | Some n -> UNameMap.add n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
-    {uctx'' with uctx_names = names; uctx_local = ctx'}, u
+    {uctx'' with uctx_names = names; uctx_local = ctx';
+      uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
 
 let new_univ_level_variable ?(template=false) ?name rigid evd =
   let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index fd299b43a..9167c9fcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -250,7 +250,7 @@ Fail Check fun A : Type => foo A.
 Check fun A : Prop => foo A.
 Fail Definition bar := fun A : Set => foo A.
 
-Check (let A := Type in foo (id A)).
+Fail Check (let A := Type in foo (id A)).
 
 Definition fooS (A : Set) := A.
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 91c58e60d..f8247c4ed 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -801,24 +801,6 @@ let solve_by_tac name evi t poly subst ctx =
   Inductiveops.control_only_guard (Global.env ()) (fst body) (*FIXME ignoring the context...*);
   (fst body), subst, entry.Entries.const_entry_universes
 
-  (* try *)
-  (*   let substref = ref (Univ.LMap.empty, Univ.UContext.empty) in *)
-  (*   Pfedit.start_proof id (goal_kind poly) evi.evar_hyps  *)
-  (*     (Universes.subst_opt_univs_constr subst evi.evar_concl, ctx) *)
-  (*   (fun subst-> substref:=subst; fun _ _ -> ()); *)
-  (*   Pfedit.by (tclCOMPLETE t); *)
-  (*   let _,(const,_,_,_) = Pfedit.cook_proof ignore in *)
-  (*     Pfedit.delete_current_proof ();  *)
-  (*     Inductiveops.control_only_guard (Global.env ()) *)
-  (* 	const.Entries.const_entry_body; *)
-  (*     let subst, ctx = !substref in *)
-  (* 	subst_univs_fn_constr (Universes.make_opt_subst subst) const.Entries.const_entry_body, *)
-  (* 	subst, const.Entries.const_entry_universes *)
-  (* with reraise -> *)
-  (*   let reraise = Errors.push reraise in *)
-  (*   Pfedit.delete_current_proof(); *)
-  (*   raise reraise *)
-
 let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in