From 940b2f972c4b3f42850e36c721564b127d30e496 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 6 Mar 2018 13:41:37 +0100
Subject: An experimental 'Show Extraction' command (grant feature wish #4129)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

 Attempt to extract the current ongoing proof (request by
 Clément Pit-Claudel on coqdev, and also #4129).
 Evars are handled as axioms.
---
 plugins/extraction/g_extraction.ml4 | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'plugins/extraction/g_extraction.ml4')

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
-- 
cgit v1.2.3