[proof] Move initial_euctx to proof_global

These are only needed when closing / admitting a proof.

1 files changed, 1 insertions, 1 deletions

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