Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 8 insertions, 5 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