Info: tactic notations (TacAlias) print their names.

Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.

3 files changed, 30 insertions, 6 deletions

diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 6d6e43b21d..01c2fde2a9 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -48,6 +48,15 @@ let enter f =
   bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
     (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
 
+let with_env t =
+  t >>= function
+    | Uniform a ->
+        Proofview.tclENV >>= fun env -> Proofview.tclUNIT (Uniform (env,a))
+    | Depends l ->
+        Proofview.Goal.goals >>= fun gs ->
+        Proofview.Monad.(List.map (map Proofview.Goal.env) gs) >>= fun envs ->
+        Proofview.tclUNIT (Depends (List.combine envs l))
+
 let lift (type a) (t:a Proofview.tactic) : a t =
   Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x))
 
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index 19ef717bc9..3102869ef9 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -44,6 +44,11 @@ val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal, without evar normalization. The resulting tactic is
     focussed. *)
 
+val with_env : 'a t -> (Environ.env*'a) t
+(** [with_env t] returns, in addition to the return type of [t], an
+    environment, which is the global environment if [t] does not focus on
+    goals, or the local goal environment if [t] focuses on goals. *)
+
 (** {5 Notations} *)
 
 val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a726253dc8..c0dac416cd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1217,18 +1217,28 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         end
       in
       let (>>=) = Ftactic.bind in
-      let addvar (x, v) accu =
-        f v >>= fun v ->
-        Ftactic.return (Id.Map.add x v accu)
+      let interp_vars =
+        Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l
       in
-      let tac = Ftactic.List.fold_right addvar l ist.lfun >>= fun lfun ->
+      let addvar (x, v) accu = Id.Map.add x v accu in
+      let tac l =
+        let lfun = List.fold_right addvar l ist.lfun in
         let trace = push_trace (loc,LtacNotationCall s) ist in
         let ist = {
           lfun = lfun;
           extra = TacStore.set ist.extra f_trace trace; } in
-        val_interp ist body
+        val_interp ist body >>= fun v ->
+        Ftactic.lift (tactic_of_value ist v)
       in
-      Ftactic.run tac (fun v -> tactic_of_value ist v)
+      let tac =
+        Ftactic.with_env interp_vars >>= fun (env,l) ->
+        let name () = Pptactic.pr_tactic env (TacAlias(loc,s,l)) in
+        Proofview.Trace.name_tactic name (tac l)
+      (* spiwack: this use of name_tactic is not robust to a
+         change of implementation of [Ftactic]. In such a situation,
+         some more elaborate solution will have to be used. *)
+      in
+      Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
   | TacML (loc,opn,l) when List.for_all global_genarg l ->
       let trace = push_trace (loc,LtacMLCall tac) ist in