From 600fef9a1c9cd15ad43196b7750ba15922c01752 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 3 Mar 2019 01:07:19 +0100
Subject: [ssr] under: Simplify the over tactic

* Use ssr `by […|…]` and `apply:`
---
 plugins/ssr/ssreflect.v | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

(limited to 'plugins')

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