diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 6de20c64a5..31fc54c1fa 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -694,17 +694,17 @@ GRAMMAR EXTEND Gram | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] -> { match ud with | None -> - VernacCanonical CAst.(make ~loc @@ AN qid) + VernacCanonical CAst.(make ?loc:qid.CAst.loc @@ AN qid) | Some (u,d) -> let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) } + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) } | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation -> { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) } (* Coercions *) | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body -> { let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) } + VernacDefinition ((NoDischarge,Coercion),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) } | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> { VernacIdentityCoercion (f, s, t) } |