- Fix in kernel conversion not folding the universe constraints

correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.

2 files changed, 18 insertions, 5 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 9cbd89e8b8..0668af2c50 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -170,8 +170,6 @@ let look_for_possibly_mutual_statements = function
 let save id const cstrs do_guard (locality,poly,kind) hook =
   let const = adjust_guardness_conditions const do_guard in
   let k = Kindops.logical_kind_of_goal_kind kind in
-  (* Add global constraints necessary to check the type of the proof *)
-  let () = Global.push_context (snd cstrs) in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
 	let c = SectionLocalDef const in
@@ -316,13 +314,14 @@ let standard_proof_terminator compute_guard hook =
           save_anonymous_with_strength proof kind id
       end
 
-let standard_proof_terminator compute_guard hook =
+let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
-      admit hook ();
+      admit (hook (Univ.LMap.empty, Univ.UContext.empty)) ();
       Pp.feedback Interface.AddedAxiom
   | Proved (is_opaque,idopt,proof) ->
-      let proof = get_proof proof compute_guard hook is_opaque in
+      let proof = get_proof proof compute_guard 
+	(hook proof.Proof_global.universes) is_opaque in
       begin match idopt with
       | None -> save_named proof
       | Some ((_,id),None) -> save_anonymous proof id
@@ -340,6 +339,16 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
   !start_hook (fst c);
   Pfedit.start_proof id kind sign c ?init_tac terminator
 
+let start_proof_univs id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = universe_proof_terminator compute_guard hook in
+  let sign = 
+    match sign with
+    | Some sign -> sign
+    | None -> initialize_named_context_for_proof ()
+  in
+  !start_hook (fst c);
+  Pfedit.start_proof id kind sign c ?init_tac terminator
+
 
 (* FIXME: forgetting about the universes here *)
 let rec_tac_initializer finite guard thms snl =
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index f8694a0961..8f5c75976a 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -21,6 +21,10 @@ val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
+val start_proof_univs : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types Univ.in_universe_context_set ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  (Proof_global.proof_universes -> unit declaration_hook) -> unit
+
 val start_proof_com : goal_kind ->
   (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
   unit declaration_hook -> unit