diff options
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 468f2fe8c..93909f3e6 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -160,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> [ show_extraction () ] +END |