From 2c5ed1c5afe5f1270e842f161a005e253d31eb85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 1 Sep 2015 12:20:32 +0200
Subject: Hacking parser so as to support both [> ... ] and [id].

This (at least technically) solves the issue #4113 (see also #4329).
---
 parsing/g_vernac.ml4 | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fe9c582408..11f78c708c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -71,6 +71,17 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -129,7 +140,7 @@ GEXTEND Gram
 
   selector:
     [ [ n=natural; ":" -> SelectNth n
-      | "["; id = ident; "]"; ":" -> SelectId id
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
       | IDENT "all" ; ":" -> SelectAll
       | IDENT "par" ; ":" -> SelectAllParallel ] ]
   ;
-- 
cgit v1.2.3