diff options
| author | Matthieu Sozeau | 2018-06-05 12:08:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-06-05 12:08:08 +0200 |
| commit | af65c79cc976f3f96a768f3d0897febb24e1485a (patch) | |
| tree | 13a928e685c5def05ce57eb3227eca75286bc8ba | |
| parent | 56be411d5c582d6f644129dabda7ba036a4419a7 (diff) | |
| parent | 160e9f8c7d1af2357db4a37d834b0b9bb28632fb (diff) | |
Merge PR #7453: Refuse to parse empty [Context] command.
| -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 dd8149d0a1..b6523981c7 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"; |