1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v
new file mode 100644
index 00000000..3f6b9cb3
--- /dev/null
+++ b/test-suite/success/shrink_abstract.v
@@ -0,0 +1,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).