aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 21:24:04 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 21:24:04 +0100
commit374d1efc5de20f8c99c13a7216357a7228c353e8 (patch)
tree57c77f168c5b5e0d8164128d7977e2bd0efdfc7f /test-suite
parenta40fb961c8ffeeb03769404cacda8bd6cff17417 (diff)
parent940b2f972c4b3f42850e36c721564b127d30e496 (diff)
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish #4129)
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/ShowExtraction.v31
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.