[ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc

* Add tests accordingly.

3 files changed, 21 insertions, 4 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2bac69b5b7..d60e3857b1 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -406,7 +406,15 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let undertac ist ipats ((dir,_),_ as rule) hint =
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
+let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
+
+  (* total number of implied hints *)
+  let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
 
   let varnames =
     let rec aux acc = function
@@ -426,7 +434,11 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
   let ipats =
     match ipats with
     | None -> [IPatNoop]
+    | Some l when pad_intro -> (* typically, ipats = Some [IPatAnon All] *)
+       let new_l = ncons (nh - 1) l in
+       [IPatCase(Regular (new_l @ [[]]))]
     | Some (IPatCase(Regular []) :: _ as ipats) -> ipats
+    (* Erik: is the previous line correct/useful? *)
     | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest
     | Some (IPatCase(Block _) :: _ as l) -> l
     | Some l -> [IPatCase(Regular [l;[]])] in
@@ -457,7 +469,6 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
       Proofview.tclUNIT ()
     else
       let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
-      let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
       (* Usefulness of check_numgoals: tclDISPATCH would be enough,
          except for the error message w.r.t. the number of
          provided/expected tactics, as the last one is implied *)
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 6f7cc6d445..6dd01ca6fc 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,7 +57,13 @@ val sufftac :
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
+(* pad_intro (by default false) indicates whether the intro-pattern
+   "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches,
+   assuming there are n provided tactics in the ssrhint argument
+   "do [...|...|...]"; it is useful when the intro-pattern is "=> *").
+   Otherwise, "=> i..." is turned into "=> [i...|]". *)
 val undertac :
+  ?pad_intro:bool ->
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 2c46947658..4286ace519 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2690,9 +2690,9 @@ TACTIC EXTEND under
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg h
     }
-  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *)
+  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *)
     check_under_arg arg;
-    Ssrfwd.undertac ist (Some [IPatAnon All]) arg h
+    Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
 END