diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 15:59:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 16:44:30 +0200 |
| commit | f27df397b49d2bb469e513749cade21e5c259926 (patch) | |
| tree | 995eefeb3129ce9bb773597bf2c2548793350eb5 /library | |
| parent | 32ea597251d4fc7cfbab26022a5355949e8a3257 (diff) | |
Adding a new "Locate Term" command, distinct from the raw "Locate" command.
The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".
Fixes bug #3380.
Diffstat (limited to 'library')
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 4a61a9540..edceacaa8 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -429,6 +429,8 @@ let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab +let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab + (* Derived functions *) let locate_constant qid = diff --git a/library/nametab.mli b/library/nametab.mli index ed4200456..1289a6745 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -112,6 +112,7 @@ val global_inductive : reference -> inductive val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_tactic : qualid -> ltac_constant list +val locate_extended_all_dir : qualid -> global_dir_reference list (** Mapping a full path to a global reference *) |