Remove the syntax [Vernac1. Vernac2. … Vernacn. ].

It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.

The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].

I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.

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 ] ]
   ;