diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 15:09:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 18:59:00 +0200 |
| commit | 811ed22e8dcb12d8c88e2c320bbc2221bdff30ab (patch) | |
| tree | 02fa0c79935c69c3596a9701d14134941a01f39a /intf | |
| parent | 1a6a26d29252da54b86bf663a66ddd909905d1cb (diff) | |
Implementing a generic mechanism for locating named objects from Coq side.
Diffstat (limited to 'intf')
| -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 = |