diff options
| author | Pierre-Marie Pédrot | 2014-07-21 15:59:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-21 16:44:30 +0200 |
| commit | f27df397b49d2bb469e513749cade21e5c259926 (patch) | |
| tree | 995eefeb3129ce9bb773597bf2c2548793350eb5 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 5aa9d51fc3..f620652280 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -88,6 +88,7 @@ type searchable = | SearchAbout of (bool * search_about_item) list type locatable = + | LocateAny of reference or_by_notation | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference |