diff options
Diffstat (limited to 'plugins/extraction')
| -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 487accbc9b..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_query ] [ "Show" "Extraction" ] +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] -> { show_extraction } END |