diff options
Diffstat (limited to 'vernac/g_vernac.ml4')
| -rw-r--r-- | vernac/g_vernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 0964d46ac..dd8149d0a 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -1148,8 +1148,8 @@ GEXTEND Gram [ [ "at"; n = level -> n ] ] ; constr_as_binder_kind: - [ [ "as"; IDENT "ident" -> AsIdent - | "as"; IDENT "pattern" -> AsIdentOrPattern - | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] + [ [ "as"; IDENT "ident" -> Notation_term.AsIdent + | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern + | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ] ; END |