diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ebdec85ee..bb35445ce 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -78,6 +78,7 @@ type locatable = | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference + | LocateTactic of reference | LocateFile of string type goable = |