Documenting the new behaviour of the Shrink Obligations flag.

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v
new file mode 100644
index 000000000..676b97878
--- /dev/null
+++ b/test-suite/success/shrink_obligations.v
@@ -0,0 +1,28 @@
+Require Program.
+
+Obligation Tactic := idtac.
+
+Set Shrink Obligations.
+
+Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit :=
+let bar : {r | n < r} := _ in
+let qux : {r | p < r} := _ in
+let quz : m = n -> True := _ in
+tt.
+Next Obligation.
+intros m p n q.
+exists (S n); constructor.
+Qed.
+Next Obligation.
+intros m p n q.
+exists (S (S m)); constructor.
+Qed.
+Next Obligation.
+intros m p n q ? ? H.
+destruct H.
+constructor.
+Qed.
+
+Check (foo_obligation_1 : forall n, {r | n < r}).
+Check (foo_obligation_2 : forall m, {r | (S m) < r}).
+Check (foo_obligation_3 : forall m n, m = n -> True).