proof_global: cleanup and comment close_proof

evd: Move constrain_variables to an operation on UState

Necessary to check universe declarations correctly for deferred proofs
in particular.

1 files changed, 39 insertions, 39 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e8266f5c8..cd4d1dcf6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -318,8 +318,7 @@ let get_open_goals () =
 
 let constrain_variables init uctx =
   let levels = Univ.Instance.levels (Univ.UContext.instance init) in
-  let cstrs = UState.constrain_variables levels uctx in
-  Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
+  UState.constrain_variables levels uctx
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
@@ -332,6 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
+  let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+  let binders = if poly then Some binders else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -355,55 +356,54 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = constrain_variables 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. *)
+             complement the univ constraints of the typ with the ones of
+             the body.  So we keep the two sets distinct. *)
 	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = Univops.restrict_universe_context ctx used_univs in
-          (initunivs, typ), ((body, ctx_body), eff)
+          let ctx_body = UState.restrict ctx used_univs in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+          (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
         else
-          let initunivs = Univ.UContext.empty in
-          let ctx = constrain_variables initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
-           * constraints in which we merge the ones for the body and the ones
-           * for the typ *)
+             constraints in which we merge the ones for the body and the ones
+             for the typ. We recheck the declaration after restricting with
+             the actually used universes.
+             TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = Univops.restrict_universe_context ctx used_univs in
-          let univs = Univ.ContextSet.to_context ctx in
+          let ctx = UState.restrict universes used_univs in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context initial_euctx in
-        Future.from_val (initunivs, nf t),
+        Future.from_val (univctx, nf t),
         Future.chain ~pure:true p (fun (pt,eff) ->
-          (pt,constrain_variables initunivs (Future.force univs)),eff)
+          (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+          let bodyunivs = constrain_variables univctx (Future.force univs) in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+          (pt,Univ.ContextSet.of_context univs),eff)
   in
-  let entries =
-    Future.map2 (fun p (_, t) ->
-      let t = EConstr.Unsafe.to_constr t in
-      let univstyp, body = make_body t p in
-      let univs, typ = Future.force univstyp in
-      let univs =
-        if poly then Entries.Polymorphic_const_entry univs
-        else Entries.Monomorphic_const_entry univs
-      in
-	{ Entries.
-	  const_entry_body = body;
-	  const_entry_secctx = section_vars;
-	  const_entry_feedback = feedback_id;
-	  const_entry_type  = Some typ;
-	  const_entry_inline_code = false;
-	  const_entry_opaque = true;
-	  const_entry_universes = univs;
-        })
-		fpl initial_goals in
-  let binders =
-    if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance &&
-                    universe_decl.Misctypes.univdecl_extensible_instance) then None
-    else
-      Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl))
+  let entry_fn p (_, t) =
+    let t = EConstr.Unsafe.to_constr t in
+    let univstyp, body = make_body t p in
+    let univs, typ = Future.force univstyp in
+    let univs =
+      if poly then Entries.Polymorphic_const_entry univs
+      else Entries.Monomorphic_const_entry univs
+    in
+    {Entries.
+      const_entry_body = body;
+      const_entry_secctx = section_vars;
+      const_entry_feedback = feedback_id;
+      const_entry_type  = Some typ;
+      const_entry_inline_code = false;
+      const_entry_opaque = true;
+      const_entry_universes = univs; }
   in
+  let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
   fun pr_ending -> CEphemeron.get terminator pr_ending