diff options
| author | Erik Martin-Dorel | 2019-04-03 15:39:11 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:40 +0200 |
| commit | 36488400952da5e12c8af451b1a936a34b26039d (patch) | |
| tree | deaaf8bc97829427bf444c37ba08496874b7c356 /test-suite | |
| parent | 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 (diff) | |
[ssr] under: optimization of the tactic for (under eq_bigl => *)
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].
Also: replace "by over." in the doc example with "over."
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/under.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index ba3aa9d621..84f6b9ad03 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -90,7 +90,7 @@ under eq_bigr => i Hi. under eq_big => [j|j Hj]. { rewrite muln1. over. } { rewrite addnC. over. } -(* MISSING BETA *) + simpl. (* or: cbv beta. *) over. by []. Qed. @@ -134,7 +134,7 @@ Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) : \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. Proof. (* in one-liner mode *) -under eq_big do [move=> ? (* due to delta-head-cst *); rewrite addnC +under eq_big do [rewrite addnC |rewrite addnC]. (* amounts to [under eq_big => [*|*] do [...|...]] *) done. |