aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/shrink_abstract.v
blob: 3f6b9cb39f41836b4738d911d48f26ebe05f8900 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Set Shrink Abstract.

Definition foo : forall (n m : nat), bool.
Proof.
pose (p := 0).
intros n.
pose (q := n).
intros m.
pose (r := m).
abstract (destruct m; [left|right]).
Defined.

Check (foo_subproof : nat -> bool).