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.

1 files changed, 2 insertions, 4 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 6c963bf70..254aa8f78 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