diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 15:06:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (patch) | |
| tree | e981dabe208b339db88188b7a5e89c53d77745a1 /parsing/pcoq.mli | |
| parent | a9d151a31937724543d5269e72b0262c8764c46e (diff) | |
[location] Use located in misctypes.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 4248db697..959e8ddf5 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -206,7 +206,7 @@ module Prim : val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry - val by_notation : (Loc.t * string * string option) Gram.entry + val by_notation : (string * string option) Loc.located Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry |