From 92e2bb2bebc99b6a72ea0babad9a1c374129a0c0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 16 Apr 2019 03:18:03 +0200
Subject: [ssr] set under's tactic argument at LEVEL 3

So if the underlying tactic "contains a ;" one should actually write:

    under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
---
 test-suite/output/ssr_under.v | 2 +-
 test-suite/ssr/under.v        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v
index 7335c87e61..fb7503d902 100644
--- a/test-suite/output/ssr_under.v
+++ b/test-suite/output/ssr_under.v
@@ -10,7 +10,7 @@ Axiom eq_G :
 Ltac show := match goal with [|-?g] => idtac g end.
 
 Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-under eq_G => m do show; rewrite subnn.
+under eq_G => m do [show; rewrite subnn].
 show.
 Abort.
 
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 84f6b9ad03..f285ad138b 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -175,7 +175,7 @@ Qed.
 Lemma test_big_andb (F : nat -> nat) (m n : nat) :
   \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1.
 Proof.
-under eq_bigl => i do rewrite andb_idl; first by move/eqP->.
+under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
 under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *)
 myadmit.
 Qed.
-- 
cgit v1.2.3