[ssr] under: optimization of the tactic for (under eq_bigl => *)

so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].

Also: replace "by over." in the doc example with "over."

3 files changed, 20 insertions, 14 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a40dfa486f..4e40df6f94 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3733,7 +3733,7 @@ Let us redo the running example in interactive mode.
       Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
       under eq_map => m.
         rewrite subnn.
-        by over.
+        over.
 
 The execution of the Ltac expression:
 
@@ -3751,8 +3751,9 @@ involves the following steps:
    while the other ones correspond to premises of the rewrite rule (such as
    ``forall n, F1 n = F2 n`` for ``eq_map``).
 
-3. If so :tacn:`under` executes the corresponding
-   intro pattern :n:`@ipat__i` in each goal.
+3. If so :tacn:`under` puts these n goals in head normal form (using
+   the defective form of the tactic :tacn:`move`), then executes
+   the corresponding intro pattern :n:`@ipat__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
    are (quantified) equalities or double implications between a
@@ -3805,7 +3806,7 @@ The Ltac expression:
 
 can be seen as a shorter form for the following expression:
 
-:n:`under @term => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
+:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
 
 Notes:
 
@@ -3822,10 +3823,12 @@ Notes:
   preferred.
 
 + If the ``do`` clause is provided and the intro pattern is omitted,
-  then the defeault :token:`i_item` ``*`` is applied to each branch.
+  then the default :token:`i_item` ``*`` is applied to each branch.
   E.g., the Ltac expression:
   :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
-  :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].`
+  :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]`
+  (and it can be noted here that the :tacn:`under` tactic performs a
+  ``move.`` before processing the intro patterns ``=> [ * | … | * ]``).
 
 .. example::
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 313b46ddc3..01d71aa96a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -331,7 +331,15 @@ let is_app_evar sigma t =
       | _ -> false end
   | _ -> false
 
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
 let intro_lock ipats =
+  let hnf' = Proofview.numgoals >>= fun ng ->
+             Proofview.tclDISPATCH
+               (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
   let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
     Proofview.tclORELSE
       (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
@@ -372,7 +380,7 @@ let intro_lock ipats =
        end)
     end
   in
-  Ssripats.tclIPATssr ipats <*> lock_eq ()
+  hnf' <*> Ssripats.tclIPATssr ipats <*> lock_eq ()
 
 let pretty_rename evar_map term varnames =
   let rec aux term vars =
@@ -406,11 +414,6 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-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 *)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index ba3aa9d621..84f6b9ad03 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -90,7 +90,7 @@ under eq_bigr => i Hi.
   under eq_big => [j|j Hj].
   { rewrite muln1. over. }
   { rewrite addnC. over. }
-(* MISSING BETA *)
+  simpl. (* or: cbv beta. *)
   over.
 by [].
 Qed.
@@ -134,7 +134,7 @@ Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) :
   \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
 Proof.
 (* in one-liner mode *)
-under eq_big do [move=> ? (* due to delta-head-cst *); rewrite addnC
+under eq_big do [rewrite addnC
                 |rewrite addnC].
 (* amounts to [under eq_big => [*|*] do [...|...]] *)
 done.