[declare] Factor out universe computation in close_proof

A step towards enforcing some more static invariants.

1 files changed, 34 insertions, 33 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5be819e109..35ecb614b9 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -199,6 +199,39 @@ let prepare_proof ~unsafe_typ { proof } =
   let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
   proofs, Evd.evar_universe_context evd
 
+let make_univs ~poly ~initial_euctx ~uctx ~opaque ~udecl ~allow_deferred typ body =
+
+  let used_univs_body = Vars.universes_of_constr body in
+  let used_univs_typ = Vars.universes_of_constr typ in
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  if allow_deferred then
+    let utyp = UState.univ_entry ~poly initial_euctx in
+    let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx 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 uctx_body = UState.restrict uctx used_univs in
+    let ubody = UState.check_mono_univ_decl uctx_body udecl in
+    utyp, ubody
+  else if poly && opaque && private_poly_univs () then
+    let universes = UState.restrict uctx used_univs in
+    let typus = UState.restrict universes used_univs_typ in
+    let utyp = UState.check_univ_decl ~poly typus udecl in
+    let ubody = Univ.ContextSet.diff
+        (UState.context_set universes)
+        (UState.context_set typus)
+    in
+    utyp, ubody
+  else
+    (* 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. We recheck the declaration after restricting with
+       the actually used universes.
+       TODO: check if restrict is really necessary now. *)
+    let ctx = UState.restrict uctx used_univs in
+    let utyp = UState.check_univ_decl ~poly ctx udecl in
+    utyp, Univ.ContextSet.empty
+
 let close_proof ~opaque ~keep_body_ucst_separate ps =
 
   let { section_vars; proof; udecl; initial_euctx } = ps in
@@ -208,44 +241,12 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let opaque = match opaque with Opaque -> true | Transparent -> false in
 
   let make_entry ((body, eff), typ) =
-
     let allow_deferred =
       not poly &&
       (keep_body_ucst_separate
        || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
     in
-    let used_univs_body = Vars.universes_of_constr body in
-    let used_univs_typ = Vars.universes_of_constr typ in
-    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-    let utyp, ubody =
-      if allow_deferred then
-        let utyp = UState.univ_entry ~poly initial_euctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx 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 uctx_body = UState.restrict uctx used_univs in
-        let ubody = UState.check_mono_univ_decl uctx_body udecl in
-        utyp, ubody
-      else if poly && opaque && private_poly_univs () then
-        let universes = UState.restrict uctx used_univs in
-        let typus = UState.restrict universes used_univs_typ in
-        let utyp = UState.check_univ_decl ~poly typus udecl in
-        let ubody = Univ.ContextSet.diff
-            (UState.context_set universes)
-            (UState.context_set typus)
-        in
-        utyp, ubody
-      else
-        (* 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. We recheck the declaration after restricting with
-           the actually used universes.
-           TODO: check if restrict is really necessary now. *)
-        let ctx = UState.restrict uctx used_univs in
-        let utyp = UState.check_univ_decl ~poly ctx udecl in
-        utyp, Univ.ContextSet.empty
-    in
+    let utyp, ubody = make_univs ~initial_euctx ~poly ~opaque ~uctx ~allow_deferred ~udecl typ body in
     definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in