1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 05e6549255..3c3caa140b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -69,7 +69,7 @@ let default_command_entry =
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
-    [ [ IDENT "Time"; v = vernac -> VernacTime v
+    [ [ IDENT "Time"; l = vernac_list -> VernacTime l
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
@@ -104,10 +104,12 @@ GEXTEND Gram
       | g = gallina_ext; "." -> g
       | c = command; "." -> c
       | c = syntax; "." -> c
-      | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
       | c = subprf -> c
     ] ]
   ;
+  vernac_list:
+    [ [ c = located_vernac -> [c] ] ]
+  ;
   vernac_aux: LAST
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;