Useless keeping of dirpath in tactic aliases.

4 files changed, 11 insertions, 14 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 5ce914a9c8..073df91cfa 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -17,10 +17,10 @@ open Tacexpr
 type alias = KerName.t
 
 let alias_map = Summary.ref ~name:"tactic-alias"
-  (KNmap.empty : (DirPath.t * glob_tactic_expr) KNmap.t)
+  (KNmap.empty : glob_tactic_expr KNmap.t)
 
-let register_alias key dp tac =
-  alias_map := KNmap.add key (dp, tac) !alias_map
+let register_alias key tac =
+  alias_map := KNmap.add key tac !alias_map
 
 let interp_alias key =
   try KNmap.find key !alias_map
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index dcc2146f9b..a7609ae215 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -17,10 +17,10 @@ open Tacexpr
 type alias = KerName.t
 (** Type of tactic alias, used in the [TacAlias] node. *)
 
-val register_alias : alias -> DirPath.t -> glob_tactic_expr -> unit
+val register_alias : alias -> glob_tactic_expr -> unit
 (** Register a tactic alias. *)
 
-val interp_alias : alias -> (DirPath.t * glob_tactic_expr)
+val interp_alias : alias -> glob_tactic_expr
 (** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
 
 (** {5 Coq tactic definitions} *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 97cb50a286..cd38f6768f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1823,7 +1823,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         tac args ist
       end
   | TacAlias (loc,s,l) ->
-      let (_, body) = Tacenv.interp_alias s in
+      let body = Tacenv.interp_alias s in
       let rec f x = match genarg_tag x with
       | QuantHypArgType | RedExprArgType
       | ConstrWithBindingsArgType
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a398b77774..6f6bfc52e7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,12 +65,11 @@ type tactic_grammar_obj = {
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
-  tacobj_body : DirPath.t * Tacexpr.glob_tactic_expr
+  tacobj_body : Tacexpr.glob_tactic_expr
 }
 
 let cache_tactic_notation ((_, key), tobj) =
-  let (dp, body) = tobj.tacobj_body in
-  Tacenv.register_alias key dp body;
+  Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
@@ -79,16 +78,14 @@ let open_tactic_notation i ((_, key), tobj) =
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
 let load_tactic_notation i ((_, key), tobj) =
-  let (dp, body) = tobj.tacobj_body in
   (** Only add the printing and interpretation rules. *)
-  Tacenv.register_alias key dp body;
+  Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
   if Int.equal i 1 && not tobj.tacobj_local then
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  let dir, tac = tobj.tacobj_body in
-  { tobj with tacobj_body = (dir, Tacsubst.subst_tactic subst tac); }
+  { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; }
 
 let classify_tactic_notation tacobj = Substitute tacobj
 
@@ -121,7 +118,7 @@ let add_tactic_notation (local,n,prods,e) =
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;
-    tacobj_body = (Lib.cwd (), tac);
+    tacobj_body = tac;
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)