From 7525890df67fe711e2d3d63846ddb1e988d0812b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Sep 2014 18:13:07 +0200
Subject: Fixing bug #2818.

Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
---
 library/nametab.ml  |  2 ++
 library/nametab.mli |  1 +
 tactics/tacenv.ml   | 17 ++++++++++++-----
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/library/nametab.ml b/library/nametab.ml
index 3bd4e03abf..390789852e 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -470,6 +470,8 @@ let exists_module = exists_dir
 
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
+let exists_tactic kn = KnTab.exists kn !the_tactictab
+
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
diff --git a/library/nametab.mli b/library/nametab.mli
index eb2cecc59b..e508c8617f 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -127,6 +127,7 @@ val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
 val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
 val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *)
 
 (** {6 These functions locate qualids into full user names } *)
 
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 4c8175b8dd..8557ee6a80 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -85,14 +85,22 @@ let add (kn,td) = mactab := KNmap.add kn td !mactab
 let replace (kn,td) = mactab := KNmap.add kn td !mactab
 
 let load_md i ((sp, kn), (local, id ,t)) = match id with
-| None -> Nametab.push_tactic (Until i) sp kn; add (kn, t)
+| None ->
+  let () = if not local then Nametab.push_tactic (Until i) sp kn in
+  add (kn, t)
 | Some kn -> add (kn, t)
 
 let open_md i ((sp, kn), (local, id ,t)) = match id with
-| None -> Nametab.push_tactic (Exactly i) sp kn; add (kn, t)
+| None ->
+  let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
+  add (kn, t)
 | Some kn -> add (kn, t)
 
-let cache_md x = load_md 1 x
+let cache_md ((sp, kn), (local, id ,t)) = match id with
+| None ->
+  let () = Nametab.push_tactic (Until 1) sp kn in
+  add (kn, t)
+| Some kn -> add (kn, t)
 
 let subst_kind subst id = match id with
 | None -> None
@@ -101,8 +109,7 @@ let subst_kind subst id = match id with
 let subst_md (subst, (local, id, t)) =
   (local, subst_kind subst id, Tacsubst.subst_tactic subst t)
 
-let classify_md (local, _, _ as o) =
-  if local then Dispose else Substitute o
+let classify_md (local, _, _ as o) = Substitute o
 
 let inMD : bool * Nametab.ltac_constant option * glob_tactic_expr -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
-- 
cgit v1.2.3