From 160e9f8c7d1af2357db4a37d834b0b9bb28632fb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 7 May 2018 22:20:09 +0200
Subject: Refuse to parse empty [Context] command.

The error is now:
    Syntax error: [constr:binder] expected after 'Context' (in [vernac:gallina_ext]).

Close #7452.
---
 vernac/g_vernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

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";
-- 
cgit v1.2.3