diff options
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 + ]. |