Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole

proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].

This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.

1 files changed, 11 insertions, 2 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 3afbc8138e..5df373d589 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -184,7 +184,16 @@ let declare_tactic loc s c cl = match cl with
   let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
   let se = mlexpr_of_string s in
   let name = mlexpr_of_string name in
-  let tac = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+  let tac =
+    (** Special handling of tactics without arguments: such tactics do not do
+        a Proofview.Goal.enter to compute their arguments. It matters for some
+        whole-prof tactics like [shelve_unifiable]. *)
+    if List.is_empty rem then
+      <:expr< fun _ $lid:"ist"$ -> $tac$ >>
+    else
+      let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+      <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
+  in
   (** Arguments are not passed directly to the ML tactic in the TacExtend node,
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
@@ -194,7 +203,7 @@ let declare_tactic loc s c cl = match cl with
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in
       try do {
-        Tacenv.register_ml_tactic $se$ (Tacinterp.lift_constr_tac_to_ml_tac $vars$ $tac$);
+        Tacenv.register_ml_tactic $se$ $tac$;
         Mltop.declare_cache_obj obj __coq_plugin_name; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning