From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 May 2019 19:46:02 +0200
Subject: Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.
---
 plugins/extraction/extract_env.ml   | 4 ----
 plugins/extraction/extract_env.mli  | 2 +-
 plugins/extraction/g_extraction.mlg | 8 +++++++-
 3 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 8f17f7b2dd..c5439ffaf6 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -751,10 +751,6 @@ let extract_and_compile l =
 
 (* Show the extraction of the current ongoing proof *)
 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 pstate in
   let sigma, env = Pfedit.get_current_context pstate in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7ba7e05019..efd5b5575f 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 : pstate:Proof_global.t option -> unit
+val show_extraction : pstate:Proof_global.pstate -> unit
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index db1a389fe7..d43d90af60 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -179,5 +179,11 @@ END
 
 VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
 | ![ proof ] [ "Show" "Extraction" ]
-  -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
+  -> { fun ~pstate:ontop ->
+    let pstate = Option.map Proof_global.get_current_pstate ontop in
+    let pstate = match pstate with
+      | None -> CErrors.user_err Pp.(str "No ongoing proof")
+      | Some pstate -> pstate
+    in
+    let () = show_extraction ~pstate in ontop }
 END
-- 
cgit v1.2.3