diff options
| author | Erik Martin-Dorel | 2019-03-03 01:07:19 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:44 +0200 |
| commit | 600fef9a1c9cd15ad43196b7750ba15922c01752 (patch) | |
| tree | 72f516bdba187eedb3b9895ef702d563fb292c9f /plugins | |
| parent | c9454e2f4a083006d7145389beabcf8e4b10caa9 (diff) | |
[ssr] under: Simplify the over tactic
* Use ssr `by […|…]` and `apply:`
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssreflect.v | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index e1e4d25ced..37390e1af7 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -551,16 +551,6 @@ Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := - solve [ apply Under.under_done - | by rewrite over - ]. - -(* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1] - (2-var test case with evars). - -Ltac over := - exact: Under.under_done. - -Ltac over := - by rewrite over. - *) + by [ apply: Under.under_done + | rewrite over + ]. |