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

---
 user-contrib/Ltac2/tac2entries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 3b8fc58c6f..17004bb012 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -763,7 +763,7 @@ let perform_eval ~pstate e =
   | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
   in
   let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
-  let sigma = Proof.in_proof proof (fun sigma -> sigma) in
+  let { Proof.sigma } = Proof.data proof in
   let name = int_name () in
   Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty)
     ++ spc () ++  str "=" ++ spc () ++
-- 
cgit v1.2.3