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.

1 files changed, 31 insertions, 0 deletions

diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v
new file mode 100644
index 000000000..e34c240c5
--- /dev/null
+++ b/test-suite/success/ShowExtraction.v
@@ -0,0 +1,31 @@
+
+Require Extraction.
+Require Import List.
+
+Section Test.
+Variable A : Type.
+Variable decA : forall (x y:A), {x=y}+{x<>y}.
+
+(** Should fail when no proofs are started *)
+Fail Show Extraction.
+
+Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
+Proof.
+Show Extraction.
+fix 1.
+destruct xs as [|x xs], ys as [|y ys].
+Show Extraction.
+- now left.
+- now right.
+- now right.
+- Show Extraction.
+  destruct (decA x y).
+  + destruct (decListA xs ys).
+    * left; now f_equal.
+    * Show Extraction.
+      right. congruence.
+  + right. congruence.
+Show Extraction.
+Defined.
+
+End Test.