From 527e6a97d1429a58273ddc6b4ce2826df0dba1c6 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 24 Feb 2019 16:08:36 +0100
Subject: [ssr] over: also works on universally quantified goals

---
 plugins/ssr/ssreflect.v | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'plugins')

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.
+ *)
-- 
cgit v1.2.3