From f27df397b49d2bb469e513749cade21e5c259926 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Jul 2014 15:59:51 +0200 Subject: 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. --- library/nametab.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'library/nametab.mli') 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 *) -- cgit v1.2.3