diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-07 22:20:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-02 20:56:28 +0200 |
| commit | 160e9f8c7d1af2357db4a37d834b0b9bb28632fb (patch) | |
| tree | 49e5f251c2fe8d4ccd27ddd1c74b37cc6003b15c /vernac | |
| parent | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff) | |
Refuse to parse empty [Context] command.
The error is now:
Syntax error: [constr:binder] expected after 'Context' (in [vernac:gallina_ext]).
Close #7452.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index dd8149d0a..b6523981c 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -631,8 +631,8 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - | IDENT "Context"; c = binders -> - VernacContext c + | IDENT "Context"; c = LIST1 binder -> + VernacContext (List.flatten c) | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; |