diff options
Diffstat (limited to 'intf/vernacexpr.ml')
| -rw-r--r-- | intf/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 03e8ea43d..4a471d4a2 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -91,7 +91,7 @@ type locatable = | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference - | LocateTactic of reference + | LocateOther of string * reference | LocateFile of string type showable = |