diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -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 5aa9d51fc..f62065228 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 |