From 2d8f2cc01d8d35baa39144274a700a9ebc66f794 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Dec 2018 01:06:33 +0100
Subject: [plugins] [extraction] Adapt to removal of imperative proof state.

---
 plugins/extraction/extract_env.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins/extraction/extract_env.ml')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 0fa9be21c9..8f17f7b2dd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -750,16 +750,19 @@ let extract_and_compile l =
   Feedback.msg_notice (str "Extracted code successfully compiled")
 
 (* Show the extraction of the current ongoing proof *)
-
-let show_extraction () =
+let show_extraction ~pstate =
+  let pstate = match pstate with
+    | None -> CErrors.user_err Pp.(str "No ongoing proof")
+    | Some pstate -> pstate
+  in
   init ~inner:true false false;
-  let prf = Proof_global.give_me_the_proof () in
-  let sigma, env = Pfedit.get_current_context () in
+  let prf = Proof_global.give_me_the_proof pstate in
+  let sigma, env = Pfedit.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
-    let l = Label.of_id (Proof_global.get_current_proof_name ()) in
+    let l = Label.of_id (Proof_global.get_current_proof_name pstate) in
     let fake_ref = ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl
-- 
cgit v1.2.3