From ff89f99bed1ae400c4cba283b17f172ca3fe6eee Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Jun 2014 14:42:07 +0200
Subject: 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.
---
 intf/vernacexpr.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 335e04b91f..3ffaca1138 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -265,9 +265,8 @@ type module_binder = bool option * lident list * module_ast_inl
 
 type vernac_expr =
   (* Control *)
-  | VernacList of located_vernac_expr list
   | VernacLoad of verbose_flag * string
-  | VernacTime of vernac_expr
+  | VernacTime of vernac_list
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacError of exn (* always fails *)
@@ -431,6 +430,8 @@ type vernac_expr =
   | VernacPolymorphic of bool * vernac_expr
   | VernacLocal of bool * vernac_expr
 
+and vernac_list = located_vernac_expr list
+
 and located_vernac_expr = Loc.t * vernac_expr
 
 (* A vernac classifier has to tell if a command:
-- 
cgit v1.2.3