diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 94fa37eb69..ab440c6b71 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -484,7 +484,7 @@ and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit and vernac_argument_status = { name : Name.t; recarg_like : bool; - notation_scope : (Loc.t * string) option; + notation_scope : string Loc.located option; implicit_status : vernac_implicit_status; } |