3 files changed, 19 insertions, 6 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 29983e7504..570b5a8c61 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -393,7 +393,9 @@ let rec pretty_rename evar_map term = function
         ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
         term
 
-let undertac ist varnames ((dir,mult),_ as rule) =
+let overtac gl = ssr_n_tac "over" ~-1 gl
+
+let undertac ist varnames ((dir,mult),_ as rule) hint =
   if mult <> Ssrequality.nomult then
     Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
 
@@ -418,5 +420,15 @@ let undertac ist varnames ((dir,mult),_ as rule) =
     ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
     evar_map, new_t
   in
-  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
-  intro_lock varnames
+  let undertacs =
+    if hint = nohint then
+      Proofview.tclUNIT ()
+    else
+      Proofview.tclDISPATCH
+        ((List.map (function None -> Proofview.V82.tactic overtac
+                           | Some e -> ssrevaltac ist e <*>
+                                         Proofview.V82.tactic overtac)
+            (if hint = nullhint then [None] else snd hint)) @ [Proofview.tclUNIT ()])
+  in
+  (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
+     intro_lock varnames <*> undertacs)
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index fe7d84871e..63df8f5349 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -59,4 +59,5 @@ val sufftac :
 
 val undertac :
   Ltac_plugin.Tacinterp.interp_sign ->
-  Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic
+  Names.Id.t list -> 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 e63d1e5562..507cf8db70 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2651,8 +2651,8 @@ TACTIC EXTEND ssrgenhave2
 END
 
 TACTIC EXTEND under
-  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] ->
-    { Ssrfwd.undertac ist names r }
+  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] ->
+    { Ssrfwd.undertac ist names r hint }
 END
 
 {