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, 9 insertions, 3 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 8ba01a7b2..05c8fdd0d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,7 +56,7 @@ let undo_classifier = ref (fun _ -> assert false)
 let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
-  let static_classifier e = match e with
+  let rec static_classifier e = match e with
     (* PG compatibility *)
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
@@ -77,7 +77,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e -> classify_vernac e
+    | VernacTime e -> classify_vernac_list e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep | VtSideff _
@@ -157,7 +157,6 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
-    | VernacList _
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
     | VernacEndSegment _ -> VtSideff [], VtNow
@@ -193,6 +192,13 @@ let rec classify_vernac e =
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str s)
+  and classify_vernac_list = function
+    (* spiwack: It would be better to define a monoid on classifiers.
+       So that the classifier of the list would be the composition of
+       the classifier of the individual commands. Currently: special
+       case for singleton lists.*)
+    | [_,c] -> static_classifier c
+    | l -> VtUnknown,VtNow
   in
   let res = static_classifier e in
     if Flags.is_universe_polymorphism () then