diff options
| -rw-r--r-- | parsing/g_prim.mlg | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 7e0360af72..389d3f581f 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -82,11 +82,6 @@ GRAMMAR EXTEND Gram | id = ident -> { CAst.make ~loc [id] } ] ] ; - basequalid: - [ [ id = ident; f=fields -> { let (l,id') = f in local_make_qualid loc (l@[id]) id' } - | id = ident -> { qualid_of_ident ~loc id } - ] ] - ; name: [ [ IDENT "_" -> { CAst.make ~loc Anonymous } | id = ident -> { CAst.make ~loc @@ Name id } ] ] @@ -95,9 +90,12 @@ GRAMMAR EXTEND Gram [ [ id = ident; f = fields -> { let (l,id') = f in local_make_qualid loc (l@[id]) id' } - | id = ident -> { local_make_qualid loc [] id } + | id = ident -> { qualid_of_ident ~loc id } ] ] ; + qualid: (* Synonymous to reference *) + [ [ qid = reference -> { qid } ] ] + ; by_notation: [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ] ; @@ -105,9 +103,6 @@ GRAMMAR EXTEND Gram [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c } | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ] ; - qualid: - [ [ qid = basequalid -> { qid } ] ] - ; ne_string: [ [ s = STRING -> { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s } |