4 files changed, 12 insertions, 9 deletions
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/extraction.ml b/plugins/extraction/extraction.ml
index c9cfd74362..9db7c8d8d3 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = constructors_nrealargs_env env ip in
+  let ni = constructors_nrealargs env ip in
   let br_size = Array.length br in
   assert (Int.equal (Array.length ni) br_size);
   if Int.equal br_size 0 then begin
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