CLEANUP: Vernacexpr.vernac_expr

Originally, "VernacTime" and "VernacRedirect" were defined like this:

      type vernac_expr =
      ...
      | VernacTime of vernac_list
      | VernacRedirect of string * vernac_list
      ...

where

      type vernac_list = located_vernac_expr list

Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:

      | VernacTime of located_vernac_expr
      | VernacRedirect of string * located_vernac_expr

which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.

3 files changed, 8 insertions, 15 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ea669b1596..e0e7875036 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
+    | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
     | _ -> false in
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -1501,7 +1501,7 @@ end = struct (* {{{ *)
     let e, etac, time, fail =
       let rec find time fail = function
         | VernacSolve(_,_,re,b) -> re, b, time, fail
-        | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
+        | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
         | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index b912080413..95aaea6f00 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -487,12 +487,12 @@ let rec tmpp v loc =
   (* Control *)
   | VernacLoad (verbose,f) ->
       xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
-  | VernacTime l ->
+  | VernacTime (loc,e) ->
       xmlApply loc (Element("time",[],[]) ::
-                    List.map (fun(loc,e) ->tmpp e loc) l)
-  | VernacRedirect (s, l) ->
+                    [tmpp e loc])
+  | VernacRedirect (s, (loc,e)) ->
       xmlApply loc (Element("redirect",["path", s],[]) ::
-                      List.map (fun(loc,e) ->tmpp e loc) l)
+                    [tmpp e loc])
   | VernacTimeout (s,e) ->
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a898c687be..32358c592b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -86,7 +86,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
+    | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
@@ -175,7 +175,7 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
-    | VernacDeclareTacticDefinition (_,l) ->
+    | VernacDeclareTacticDefinition l ->
         let open Libnames in
         VtSideff (List.map (function
           | (Ident (_,r),_,_) -> r
@@ -217,13 +217,6 @@ let rec classify_vernac e =
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst 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