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

1 files changed, 9 insertions, 6 deletions

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 *)