test-suite/success/shrink_abstract.v


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).