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.

1 files changed, 5 insertions, 0 deletions

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