Hacking parser so as to support both [> ... ] and [id].

This (at least technically) solves the issue #4113 (see also #4329).

1 files changed, 12 insertions, 1 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fe9c58240..11f78c708 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 ] ]
   ;