diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 13:41:37 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 19:39:35 +0100 |
| commit | 940b2f972c4b3f42850e36c721564b127d30e496 (patch) | |
| tree | f78dd9dae78e3058a42d862540d5f5cf26a48d31 /plugins/extraction/g_extraction.ml4 | |
| parent | 8127e69a678f138ea201ec1251990b1615cb27bc (diff) | |
An experimental 'Show Extraction' command (grant feature wish #4129)
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
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 4b6de58bd..8d268d27c 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -158,3 +158,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 |