diff options
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 1 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 17 |
3 files changed, 15 insertions, 5 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 3bd4e03ab..390789852 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 eb2cecc59..e508c8617 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 4c8175b8d..8557ee6a8 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 |