diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
| commit | 374d1efc5de20f8c99c13a7216357a7228c353e8 (patch) | |
| tree | 57c77f168c5b5e0d8164128d7977e2bd0efdfc7f /plugins/extraction/g_extraction.ml4 | |
| parent | a40fb961c8ffeeb03769404cacda8bd6cff17417 (diff) | |
| parent | 940b2f972c4b3f42850e36c721564b127d30e496 (diff) | |
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish #4129)
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 |