diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssreflect.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index d2b44a869a..e705942c36 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -571,6 +571,14 @@ Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := - by apply Under.under_done. -(* [exact: Under.under_done] woud be more satisfying, - but issue with 2-var test-suite (test_over_2_2) *) + solve [ apply Under.under_done | by rewrite over ]. + +(* The 2 variants below wouldn't work for the [test_over_2_1] test + (2-var case with evars) + +Ltac over := + exact: Under.under_done. + +Ltac over := + by rewrite over. + *) |