[proof] Move initial_euctx to proof_global

These are only needed when closing / admitting a proof.

5 files changed, 33 insertions, 29 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 47502fe402..9f2c90c375 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -118,8 +118,6 @@ type t =
   (** List of goals that have been shelved. *)
   ; given_up : Goal.goal list
   (** List of goals that have been given up *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
@@ -290,14 +288,12 @@ let unfocused = is_last_focus end_of_stack_kind
 
 let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -305,14 +301,12 @@ let start ~name ~poly sigma goals =
 
 let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -488,15 +482,13 @@ type data =
   (** A representation of the shelf  *)
   ; given_up : Evar.t list
   (** A representation of the given up goals  *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } =
+let data { proofview; focus_stack; entry; shelf; given_up; name; poly } =
   let goals, sigma = Proofview.proofview proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -507,7 +499,7 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   in
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
-  { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+  { sigma; goals; entry; stack; shelf; given_up; name; poly }
 
 let pr_proof p =
   let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 6ef34eed80..7e535a258c 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -47,8 +47,6 @@ type data =
   (** A representation of the shelf  *)
   ; given_up : Evar.t list
   (** A representation of the given up goals  *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bda83487f1..ab8d87c100 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -51,6 +51,9 @@ type t =
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
   }
 
 (*** Proof Global manipulation ***)
@@ -58,6 +61,8 @@ type t =
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
 
+let get_initial_euctx ps = ps.initial_euctx
+
 let map_proof f p = { p with proof = f p.proof }
 let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
 
@@ -89,17 +94,23 @@ let set_endline_tactic tac ps =
    can typically contain universe constraints), and with universe
    bindings [udecl]. *)
 let start_proof ~name ~udecl ~poly sigma goals =
-  { proof = Proof.start ~name ~poly sigma goals
+  let proof = Proof.start ~name ~poly sigma goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
+  ; initial_euctx
   }
 
 let start_dependent_proof ~name ~udecl ~poly goals =
-  { proof = Proof.dependent_start ~name ~poly goals
+  let proof = Proof.dependent_start ~name ~poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
+  ; initial_euctx
   }
 
 let get_used_variables pf = pf.section_vars
@@ -154,8 +165,8 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; udecl } = ps in
-  let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let Proof.{ name; poly; entry } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3ce46830fd..54d5c2087a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,6 +22,9 @@ val get_used_variables : t -> Constr.named_context option
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
 
+(** Get initial universe state *)
+val get_initial_euctx : t -> UState.t
+
 val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2dbcce2399..380ccff996 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -519,7 +519,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
             ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
       in
       let typ = EConstr.Unsafe.to_constr typ in
-      let universes = Proof.((data pftree).initial_euctx) in
+      let universes = Proof_global.get_initial_euctx lemma.proof in
       (* This will warn if the proof is complete *)
       let pproofs, _univs =
         Proof_global.return_proof ~allow_partial:true lemma.proof in