From 11cdf7c2ca0017f6bae906f9c9d9eef41972affe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 15:16:06 +0200
Subject: Univs: fix handling of side effects/delayed proofs

- When there are side effects which might enrich the initial universes
  of a proof, keep the initial and refined universe contexts apart like
  for delayed proofs, ensuring universes are declared before they are
  used in the right order.
- Fix undefined levels in proof statements so that they can't be lowered
  to Set by a subsequent, delayed proof.
---
 proofs/proof_global.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 6c963bf705..254aa8f783 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -290,16 +290,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let body = c and typ = nf t in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_separate then
+        if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
           let ctx_body = restrict_universe_context ctx used_univs_body in
-          let ctx_typ = restrict_universe_context ctx used_univs_typ in
-          let univs_typ = Univ.ContextSet.to_context ctx_typ in
-          (univs_typ, typ), ((body, ctx_body), eff)
+          (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
           let ctx = Evd.evar_universe_context_set initunivs universes in
-- 
cgit v1.2.3


From 13337793ea7f709eaa50965797e4f79a3aa51a2b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:35:44 +0200
Subject: Univs: fix handling of evd's universes and side effects in
 build_by_tactic

---
 proofs/pfedit.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 05a2975458..00ef8ecafd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -152,9 +152,9 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
   let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
+  let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
   assert(Declareops.side_effects_is_empty se);
-  assert(Univ.ContextSet.is_empty ctx);
-  cb, status, univs
+  cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
   (** Save the initial side-effects to restore them afterwards. We set the
-- 
cgit v1.2.3