diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1ac260ebeb..0fe0ac42b1 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -132,10 +132,7 @@ GEXTEND Gram closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: - [ [ id = Prim.ident -> id - - (* This is used in quotations and Syntax *) - | id = METAIDENT -> Id.of_string id ] ] + [ [ id = Prim.ident -> id ] ] ; Prim.name: [ [ "_" -> (!@loc, Anonymous) ] ] |