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 ++++++++-----
 plugins/extraction/extract_env.mli  |  2 +-
 plugins/extraction/g_extraction.mlg |  4 ++--
 3 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'plugins')

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
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 54fde2ca46..7ba7e05019 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
 
 (* Show the extraction of the current ongoing proof *)
 
-val show_extraction : unit -> unit
+val show_extraction : pstate:Proof_global.t option -> unit
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index 1445dffefa..d7bb27f121 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -178,6 +178,6 @@ END
 (* Show the extraction of the current proof *)
 
 VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| [ "Show" "Extraction" ]
-  -> { show_extraction () }
+| ![ proof ] [ "Show" "Extraction" ]
+  -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
 END
-- 
cgit v1.2.3