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.

1 files changed, 4 insertions, 4 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a0cd618e9..f61129045 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,9 +27,9 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, l) | VernacTime l ->
-    List.exists
-      (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
+  | VernacRedirect (_, (_,c))
+  | VernacTime (_,c) ->
+      is_navigation_vernac c (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
 
 and is_deep_navigation_vernac = function
@@ -229,7 +229,7 @@ let rec vernac_com verbose checknav (loc,com) =
       checknav loc com;
       if do_beautify () then pr_new_syntax loc (Some com);
       if !Flags.time then display_cmd_header loc com;
-      let com = if !Flags.time then VernacTime [loc,com] else com in
+      let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
       let (reraise, info) = Errors.push reraise in