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

1 files changed, 6 insertions, 6 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 091ab29aec..89939b864d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -285,19 +285,19 @@ let close_proof ?feedback_id ~now fpl =
 	let univsubst = (subst, Univ.ContextSet.to_context ctx) in
 	  univsubst, nf
       in
-      let make_body nf t _octx ((c, ctx), eff) =
+      let make_body nf ctx t _octx ((c, _ctx), eff) =
 	let body = nf c and typ = nf t in
 	let used_univs = 
 	  Univ.LSet.union (Universes.universes_of_constr body)
 	    (Universes.universes_of_constr typ)
 	in
-	let ctx = Universes.restrict_universe_context ctx used_univs in
+	let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) used_univs in
 	let p = (body, Univ.ContextSet.empty),eff in
 	let univs = Univ.ContextSet.to_context ctx in
 	  (univs, typ), p
       in
-      let make_body nf t octx p = 
-	Future.split2 (Future.chain ~pure:true p (make_body nf t octx))
+      let make_body nf ctx t octx p = 
+	Future.split2 (Future.chain ~pure:true p (make_body nf ctx t octx))
       in
       let univsubst =
 	Future.chain ~pure:true univs make_usubst
@@ -310,13 +310,13 @@ let close_proof ?feedback_id ~now fpl =
       in
       let univs = Univ.ContextSet.to_context ctx in
       let univsubst = (Univ.LMap.empty, univs) in
-      let make_body nf t octx p = Future.from_val (univs, t), p in
+      let make_body nf ctx t octx p = Future.from_val (univs, t), p in
 	Future.from_val (univsubst, fun x -> x), make_body
   in
   let univsubst, nf = Future.force univsubst in
   let entries =
     Future.map2 (fun p (c, (t, octx)) -> 
-      let univstyp, body = make_body nf t octx p in
+      let univstyp, body = make_body nf (snd univsubst) t octx p in
       let univs, typ = Future.force univstyp in
 	{ Entries.
 	  const_entry_body = body;