From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 26 May 2014 13:58:56 +0200
Subject: - 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.

---
 proofs/proof_global.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs')

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;
-- 
cgit v1.2.3