diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 18:58:38 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 19:19:40 +0200 |
commit | 347d94a4b966d0cc4a3a04814b0c76c4b05caa11 (patch) | |
tree | 691023e263fabdc15c02bb2e753c90a9e332ada6 /plugins/ltac/tacentries.ml | |
parent | 811ed22e8dcb12d8c88e2c320bbc2221bdff30ab (diff) |
Ltac uses the new generic locatable API.
Diffstat (limited to 'plugins/ltac/tacentries.ml')
-rw-r--r-- | plugins/ltac/tacentries.ml | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 8573da19f..bcd5b388a 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -506,6 +506,31 @@ let print_ltacs () = in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) +let locatable_ltac = "Ltac" + +let () = + let open Prettyp in + let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in + let locate_all = Tacenv.locate_extended_all_tactic in + let shortest_qualid = Tacenv.shortest_qualid_of_tactic in + let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in + let print kn = + let qid = qualid_of_path (Tacenv.path_of_tactic kn) in + Tacintern.print_ltac qid + in + let about = name in + register_locatable locatable_ltac { + locate; + locate_all; + shortest_qualid; + name; + print; + about; + } + +let print_located_tactic qid = + Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid) + (** Grammar *) let () = |