diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 2 | ||||
| -rw-r--r-- | test-suite/success/shrink_obligations.v | 28 |
3 files changed, 34 insertions, 1 deletions
@@ -26,6 +26,11 @@ Tactics - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. +Program + +- The "Shrink Obligations" flag now applies to all obligations, not only those +solved by the automatic tactic. + API - Some functions from pretyping/typing.ml and their derivatives were potential diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 8e078e981..efcc84ee9 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations defined by tactics should have their + Control whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} 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). |