diff options
Diffstat (limited to 'plugins/extraction/g_extraction.mlg')
| -rw-r--r-- | plugins/extraction/g_extraction.mlg | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d43d90af60..487accbc9b 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -178,12 +178,6 @@ END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof ] [ "Show" "Extraction" ] - -> { 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 } +| ![ proof_query ] [ "Show" "Extraction" ] + -> { show_extraction } END |