From ffaac25e993eaf103b5a66dd3b0bce7598ac8e15 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Jun 2019 15:32:06 +0200
Subject: [proof] Move initial_euctx to proof_global

These are only needed when closing / admitting a proof.
---
 vernac/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3