diff options
| author | Erik Martin-Dorel | 2018-05-29 23:07:02 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-02 20:25:00 +0200 |
| commit | bf4fdaa1836a17e4d36d38ba47959d1f50155a7b (patch) | |
| tree | 6f7270e1d61eaa47615f0cf738cc1bb6e9784947 /test-suite | |
| parent | 424c1973e96dfbf3b2e3245d735853ffa9600373 (diff) | |
[ssr] under: rewrite takes an optional bool arg
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/prerequisite/ssr_mini_mathcomp.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index cb2c56736c..ca360f65a7 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. Lemma leq_trans n m p : m <= n -> n <= p -> m <= p. Admitted. +Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p. +Admitted. Lemma leqW m n : m <= n -> m <= n.+1. Admitted. Hint Resolve leqnSn. |