diff options
Diffstat (limited to 'plugins/ltac/tacenv.ml')
-rw-r--r-- | plugins/ltac/tacenv.ml | 44 |
1 files changed, 40 insertions, 4 deletions
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 13b44f0e2..8c59a36fa 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -11,6 +11,42 @@ open Pp open Names open Tacexpr +(** Nametab for tactics *) + +(** TODO: Share me somewhere *) +module FullPath = +struct + open Libnames + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module KnTab = Nametab.Make(FullPath)(KerName) + +let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty) + +let push_tactic vis sp kn = + let (tab, revtab) = !tactic_tab in + let tab = KnTab.push vis sp kn tab in + let revtab = KNmap.add kn sp revtab in + tactic_tab := (tab, revtab) + +let locate_tactic qid = KnTab.locate qid (fst !tactic_tab) + +let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab) + +let exists_tactic kn = KnTab.exists kn (fst !tactic_tab) + +let path_of_tactic kn = KNmap.find kn (snd !tactic_tab) + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn (snd !tactic_tab) in + KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab) + (** Tactic notations (TacAlias) *) type alias = KerName.t @@ -103,19 +139,19 @@ let replace kn path t = let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Until i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Exactly i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> - let () = Nametab.push_tactic (Until 1) sp kn in + let () = push_tactic (Until 1) sp kn in add kn b t | Some kn0 -> replace kn0 kn t @@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) = let classify_md (local, _, _, _ as o) = Substitute o -let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; |