Merge PR #10215: Refine typing of vernacular commands

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares

3 files changed, 4 insertions, 8 deletions

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..7d04fee7c1 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.t -> unit
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index db1a389fe7..9ea3fbeaf4 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
 END
 (* Show the extraction of the current proof *)
 
-VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof ] [ "Show" "Extraction" ]
-  -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
+VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query
+| [ "Show" "Extraction" ]
+  -> { show_extraction }
 END