diff options
Diffstat (limited to 'plugins/extraction/g_extraction.mlg')
| -rw-r--r-- | plugins/extraction/g_extraction.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
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 |