aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ShowExtraction.v
blob: a4a35003df7c1827bf5d51311cc0e5b5336595a9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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 decListA 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.