From 2576fee1798b753161a730244c8d4d701e8a4641 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Jul 2019 04:00:11 +0200
Subject: [proof] Minor cleanup in proof.ml

---
 proofs/pfedit.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/pfedit.ml')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ed60b8274a..99a254652c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -61,8 +61,8 @@ let get_current_context pf =
   with
   | NoSuchGoal ->
     (* No more focused goals *)
-    let evd = Proof.in_proof p (fun x -> x) in
-    evd, Global.env ()
+    let { Proof.sigma } = Proof.data p in
+    sigma, Global.env ()
 
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
-- 
cgit v1.2.3