[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->].

3 files changed, 20 insertions, 4 deletions

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 4286ace519..4d65fc81d1 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -86,6 +86,15 @@ GRAMMAR EXTEND Gram
   ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
 END
 
+(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
+| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
+END
+GRAMMAR EXTEND Gram
+  GLOBAL: ssrtac3arg;
+  ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+END
+
 {
 
 (* Lexically closed tactic for tacticals. *)
@@ -1065,6 +1074,13 @@ ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintar
 | [ ssrtacarg(arg) ] -> { mk_hint arg }
 END
 
+(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
+| [ "[" "]" ] -> { nullhint }
+| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
+| [ ssrtac3arg(arg) ] -> { mk_hint arg }
+END
+
 ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 END
@@ -2686,11 +2702,11 @@ TACTIC EXTEND under
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg nohint
     }
-  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> {
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhint3arg(h) ] -> {
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg h
     }
-  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *)
+  | [ "under" ssrrwarg(arg) "do" ssrhint3arg(h) ] -> { (* implicit "=> [*|*]" *)
     check_under_arg arg;
     Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
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.