[vernac] Refactor Vernacular Control Attributes into a list

We place control attributes on their own, datatype, similarly to
regular attributes.

This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.

14 files changed, 134 insertions, 144 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7c6fa8951b..7e55eb4d13 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Unfocused"];
   ["Diffs"]]
 
-let is_known_option cmd = match Vernacprop.under_control cmd with
+let is_known_option cmd = match cmd with
   | VernacSetOption (_, o, OptionSetTrue)
   | VernacSetOption (_, o, OptionSetString _)
   | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
 
 (** Check whether a command is forbidden in the IDE *)
 
-let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
+let ide_cmd_checks ~last_valid { CAst.loc; v } =
   let user_error s =
     try CErrors.user_err ?loc ~hdr:"IDE" (str s)
     with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
       let info = Stateid.add info ~valid:last_valid Stateid.dummy in
       Exninfo.raise ~info e
   in
-  if is_debug cmd then
+  if is_debug v.expr then
     user_error "Debug mode not available in the IDE"
 
-let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
+let ide_cmd_warns ~id { CAst.loc; v } =
   let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
-  if is_known_option cmd then
+  if is_known_option v.expr then
     warn "Set this option from the IDE menu instead";
-  if is_navigation_vernac cmd || is_undo cmd then
+  if is_navigation_vernac v.expr || is_undo v.expr then
     warn "Use IDE navigation instead"
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index d220058120..92a93489f4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -180,7 +180,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacFixpoint(NoDischarge, List.map snd recsl)}))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 798c62d549..6eb8c42d1d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
 	    ++ fnl () ++
 	    msg
 	in
@@ -1532,7 +1532,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 129444c3b3..a487799b74 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -77,17 +77,18 @@ include Util
 (* ****************** - foo - bar - baz *********************************** *)
 
 let static_bullet ({ entry_point; prev_node } as view) =
+  let open Vernacexpr in
   assert (not (Vernacprop.has_Fail entry_point.ast));
-  match Vernacprop.under_control entry_point.ast with
-  | Vernacexpr.VernacBullet b ->
+  match entry_point.ast.CAst.v.expr with
+  | VernacBullet b ->
       let base = entry_point.indentation in
       let last_tac = prev_node entry_point in
       crawl view ~init:last_tac (fun prev node ->
         if node.indentation < base then `Stop else
         if node.indentation > base then `Cont node else
         if Vernacprop.has_Fail node.ast then `Stop
-        else match Vernacprop.under_control node.ast with
-        | Vernacexpr.VernacBullet b' when b = b' ->
+        else match node.ast.CAst.v.expr with
+        | VernacBullet b' when b = b' ->
           `Found { block_stop = entry_point.id; block_start = prev.id;
                    dynamic_switch = node.id; carry_on_data = of_bullet_val b }
         | _ -> `Stop) entry_point
@@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+         recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)})
       }
   | `Not -> `Leaks
 
@@ -109,16 +110,17 @@ let () = register_proof_block_delimiter
 (* ******************** { block } ***************************************** *)
   
 let static_curly_brace ({ entry_point; prev_node } as view) =
-  assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
+  let open Vernacexpr in
+  assert(entry_point.ast.CAst.v.expr = VernacEndSubproof);
   crawl view (fun (nesting,prev) node ->
     if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
-    else match Vernacprop.under_control node.ast with
-    | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+    else match node.ast.CAst.v.expr with
+    | VernacSubproof _ when nesting = 0 ->
       `Found { block_stop = entry_point.id; block_start = prev.id;
                dynamic_switch = node.id; carry_on_data = unit_val }
-    | Vernacexpr.VernacSubproof _ ->
+    | VernacSubproof _ ->
       `Cont (nesting - 1,node)
-    | Vernacexpr.VernacEndSubproof ->
+    | VernacEndSubproof ->
       `Cont (nesting + 1,node)
     | _ -> `Cont (nesting,node)) (-1, entry_point)
 
@@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+         recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof })
       }
   | `Not -> `Leaks
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 69dbebbc57..fb1c91b8af 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -571,7 +571,7 @@ end = struct (* {{{ *)
     vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
-    (match Vernacprop.under_control x with
+    (match x.CAst.v.Vernacexpr.expr with
     | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
     | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
     | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i
@@ -1078,7 +1078,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t =
     | _ -> false
   in
   (* XXX unsupported attributes *)
-  let cmd = Vernacprop.under_control expr in
+  let cmd = expr.CAst.v.expr in
   if is_filtered_command cmd then
     (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
   else begin
@@ -1141,7 +1141,7 @@ end = struct (* {{{ *)
           | { step = `Fork ((_,_,_,l),_) } -> l, false,0
           | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
           | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
-          begin match Vernacprop.under_control expr with
+          begin match expr.CAst.v.expr with
                 | VernacUndo n -> [], false, n
                 | _ -> [],false,0
           end
@@ -1171,7 +1171,7 @@ end = struct (* {{{ *)
     if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
-      match Vernacprop.under_control v with
+      match v.CAst.v.expr with
       | VernacResetInitial ->
           Stateid.initial
       | VernacResetName {CAst.v=name} ->
@@ -1977,13 +1977,14 @@ end = struct (* {{{ *)
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
     { indentation; verbose; expr = e; strlen } : unit
   =
-    let e, time, batch, fail =
-      let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function
-        | VernacTime (batch,e) -> find ~time:true ~batch ~fail e
-        | VernacRedirect (_,e) -> find ~time ~batch ~fail e
-        | VernacFail e -> find ~time ~batch ~fail:true e
-        | e -> CAst.make ?loc e, time, batch, fail) v in
-      find ~time:false ~batch:false ~fail:false e in
+    let cl, time, batch, fail =
+      let rec find ~time ~batch ~fail cl = match cl with
+        | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl
+        | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl
+        | ControlFail :: cl -> find ~time ~batch ~fail:true cl
+        | cl -> cl, time, batch, fail in
+      find ~time:false ~batch:false ~fail:false e.CAst.v.control in
+    let e = CAst.map (fun cmd -> { cmd with control = cl }) e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
@@ -2151,14 +2152,14 @@ let collect_proof keep cur hd brkind id =
    | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
    | _ -> false in
  let is_defined = function
-   | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+   | _, { expr = e } -> is_defined_expr e.CAst.v.expr
                         && (not (Vernacprop.has_Fail e)) in
  let proof_using_ast = function
    | VernacProof(_,Some _) -> true
    | _ -> false
  in
  let proof_using_ast = function
-   | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+   | Some (_, v) when proof_using_ast v.expr.CAst.v.expr
                       && (not (Vernacprop.has_Fail v.expr)) -> Some v
    | _ -> None in
  let has_proof_using x = proof_using_ast x <> None in
@@ -2167,14 +2168,14 @@ let collect_proof keep cur hd brkind id =
    | _ -> assert false
  in
  let proof_no_using = function
-   | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
+   | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v
    | _ -> assert false in
  let has_proof_no_using = function
    | VernacProof(_,None) -> true
    | _ -> false
  in
  let has_proof_no_using = function
-   | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+   | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr
                     && (not (Vernacprop.has_Fail v.expr))
    | _ -> false in
  let too_complex_to_delegate = function
@@ -2191,7 +2192,7 @@ let collect_proof keep cur hd brkind id =
     let view = VCS.visit id in
     match view.step with
     | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
-      when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+      when too_complex_to_delegate x.expr.CAst.v.expr ->
        `Sync(no_name,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
     | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
@@ -2212,7 +2213,7 @@ let collect_proof keep cur hd brkind id =
         (try
           let name, hint = name ids, get_hint_ctx loc  in
           let t, v = proof_no_using last in
-          v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr;
+          v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr;
           `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
@@ -2235,7 +2236,7 @@ let collect_proof keep cur hd brkind id =
    | _ -> false
  in
  match cur, (VCS.visit id).step, brkind with
- | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+ | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr
                                 && (not (Vernacprop.has_Fail x.expr)) ->
      `Sync (no_name,`Immediate)
  | _, _, { VCS.kind = `Edit _ }  -> check_policy (collect (Some cur) [] id)
@@ -2350,7 +2351,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
      term.` could also fail in this case, however that'd be a bug I do
      believe as proof injection shouldn't happen here. *)
   let extract_pe (x : aast) =
-    match Vernacprop.under_control x.expr with
+    match x.expr.CAst.v.expr with
     | VernacEndProof pe -> pe
     | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in
 
@@ -2873,7 +2874,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
           let queue =
             if VCS.is_vio_doc () &&
                VCS.((get_branch head).kind = `Master) &&
-               may_pierce_opaque (Vernacprop.under_control x.expr)
+               may_pierce_opaque x.expr.CAst.v.expr
             then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
@@ -2939,7 +2940,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.commit id (mkTransCmd x l true `MainQueue);
               (* We can't replay a Definition since universes may be differently
                * inferred.  This holds in Coq >= 8.5 *)
-              let action = match Vernacprop.under_control x.expr with
+              let action = match x.expr.CAst.v.expr with
                 | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
                 | _ -> ReplayCommand x in
               VCS.propagate_sideff ~action
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 5af576dad2..8d600c2859 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -202,18 +202,17 @@ let classify_vernac e =
         try Vernacextend.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let rec static_control_classifier v = v |> CAst.with_val (function
-      | VernacExpr (atts, e) ->
-        static_classifier ~atts e
-      | VernacTimeout (_,e) -> static_control_classifier e
-      | VernacTime (_,e) | VernacRedirect (_, e) ->
-        static_control_classifier e
-      | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-        (* XXX why is Fail not always Query? *)
-        (match static_control_classifier e with
+  let static_control_classifier ({ CAst.v ; _ } as cmd) =
+    (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+    (* XXX why is Fail not always Query? *)
+    if Vernacprop.has_Fail cmd then
+      (match static_classifier ~atts:v.attrs v.expr with
          | VtQuery | VtProofStep _ | VtSideff _
          | VtMeta as x -> x
          | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
-         | VtStartProof _ | VtProofMode _ -> VtQuery))
+         | VtStartProof _ | VtProofMode _ -> VtQuery)
+    else
+      static_classifier ~atts:v.attrs v.expr
+
   in
   static_control_classifier e
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index f37feb24de..78640334e2 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -340,8 +340,8 @@ let print_anyway_opts = [
 
 let print_anyway c =
   let open Vernacexpr in
-  match c with
-  | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts
+  match c.expr with
+  | VernacSetOption (_, opt, _) -> List.mem opt print_anyway_opts
   | _ -> false
 
 (* We try to behave better when goal printing raises an exception
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7a59a4dd12..e9d8263b85 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -20,14 +20,10 @@ open Vernacprop
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-let checknav_simple ({ CAst.loc; _ } as cmd) =
-  if is_navigation_vernac cmd && not (is_reset cmd) then
+let checknav { CAst.loc; v = { expr } }  =
+  if is_navigation_vernac expr && not (is_reset expr) then
     CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
 
-let checknav_deep ({ CAst.loc; _ } as cmd) =
-  if is_deep_navigation_vernac cmd then
-    CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
-
 (* Echo from a buffer based on position.
    XXX: Should move to utility file. *)
 let vernac_echo ?loc in_chan = let open Loc in
@@ -60,7 +56,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
          due to the way it prints. *)
       let com = if state.time
         then begin
-          CAst.make ?loc @@ VernacTime(state.time,com)
+          CAst.map (fun cmd -> { cmd with control = ControlTime state.time :: cmd.control }) com
         end else com in
       let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
 
@@ -108,7 +104,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
       (* Printing of AST for -compile-verbose *)
       Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
 
-      checknav_simple ast;
+      checknav ast;
 
       let state =
         Flags.silently (interp_vernac ~check ~interactive ~state) ast in
@@ -122,7 +118,6 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
     iraise (e, info)
 
 let process_expr ~state loc_ast =
-  checknav_deep loc_ast;
   interp_vernac ~interactive:true ~check:true ~state loc_ast
 
 (******************************************************************************)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dcd1979a85..54ce527ea2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -72,16 +72,29 @@ let parse_compat_version = let open Flags in function
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
 
+(* For now we just keep the top-level location of the whole
+   vernacular, that is to say, including attributes and control flags;
+   this is not very convenient for advanced clients tho, so in the
+   future it'd be cool to actually locate the attributes and control
+   flags individually too. *)
+let add_control_flag ~loc ~flag { CAst.v = cmd } =
+  CAst.make ~loc { cmd with control = flag :: cmd.control }
+
 }
 
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
   vernac_control: FIRST
-    [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
-      | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
-      | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
-      | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
-      | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
+    [ [ IDENT "Time"; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlTime false) c }
+      | IDENT "Redirect"; s = ne_string; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlRedirect s) c }
+      | IDENT "Timeout"; n = natural; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlTimeout n) c }
+      | IDENT "Fail"; c = vernac_control ->
+        { add_control_flag ~loc ~flag:ControlFail c }
+      | v = decorated_vernac ->
+        { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ]
     ]
   ;
   decorated_vernac:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0eb0b1b6f6..bd6f8f01d8 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1266,6 +1266,16 @@ let string_of_definition_object_kind = let open Decls in function
       | VernacEndSubproof ->
         return (str "}")
 
+let pr_control_flag (p : control_flag) =
+  let w = match p with
+    | ControlTime _ -> keyword "Time"
+    | ControlRedirect s -> keyword "Redirect" ++ spc() ++ qs s
+    | ControlTimeout n -> keyword "Timeout " ++ int n
+    | ControlFail -> keyword "Fail" in
+  w ++ spc ()
+
+let pr_vernac_control flags = Pp.prlist pr_control_flag flags
+
 let rec pr_vernac_flag (k, v) =
   let k = keyword k in
   let open Attributes in
@@ -1281,19 +1291,11 @@ let pr_vernac_attributes =
   | [] -> mt ()
   | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
-  let rec pr_vernac_control v =
-    let return = tag_vernac v in
-    match v.v with
-    | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
-    | VernacTime (_,v) ->
-      return (keyword "Time" ++ spc() ++ pr_vernac_control v)
-    | VernacRedirect (s, v) ->
-      return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
-    | VernacTimeout(n,v) ->
-      return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
-    | VernacFail v->
-      return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
-
-    let pr_vernac v =
-      try pr_vernac_control v
-      with e -> CErrors.print e
+let pr_vernac ({v = {control; attrs; expr}} as v) =
+  try
+    tag_vernac v
+      (pr_vernac_control control ++
+       pr_vernac_attributes attrs ++
+       pr_vernac_expr expr ++
+       sep_end expr)
+  with e -> CErrors.print e
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bc51dd46f3..2c55f73a88 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2610,7 +2610,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-and interp_expr ?proof ~atts ~st c =
+and interp_expr ~atts ~st c =
   let stack = st.Vernacstate.lemmas in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
@@ -2660,7 +2660,7 @@ and vernac_load ~verbosely fname =
     try
       let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
       let stack =
-        v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack })
+        v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
           (parse_sentence proof_mode input) in
       load_loop ~stack
     with
@@ -2673,22 +2673,23 @@ and vernac_load ~verbosely fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   ()
 
-and interp_control ?proof ~st v = match v with
-  | { v=VernacExpr (atts, cmd) } ->
+and pop_control cl = CAst.map (fun cmd -> { cmd with control = cl })
+and interp_control ~st ({ v = cmd } as vernac) = match cmd.control with
+  | [] ->
     let before_univs = Global.universes () in
-    let pstack = interp_expr ?proof ~atts ~st cmd in
+    let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
     if before_univs == Global.universes () then pstack
     else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack
-  | { v=VernacFail v } ->
-    with_fail ~st (fun () -> interp_control ?proof ~st v);
+  | ControlFail :: cl ->
+    with_fail ~st (fun () -> interp_control ~st (pop_control cl vernac));
     st.Vernacstate.lemmas
-  | { v=VernacTimeout (timeout,v) } ->
-    vernac_timeout ~timeout (interp_control ?proof ~st) v
-  | { v=VernacRedirect (s, v) } ->
-    Topfmt.with_output_to_file s (interp_control ?proof ~st) v
-  | { v=VernacTime (batch, cmd) }->
-    let header = if batch then Topfmt.pr_cmd_header cmd else Pp.mt () in
-    System.with_time ~batch ~header (interp_control ?proof ~st) cmd
+  | ControlTimeout timeout :: cl ->
+    vernac_timeout ~timeout (interp_control ~st) (pop_control cl vernac)
+  | ControlRedirect s :: cl ->
+    Topfmt.with_output_to_file s (interp_control ~st) (pop_control cl vernac)
+  | ControlTime batch :: cl ->
+    let header = if batch then Topfmt.pr_cmd_header vernac else Pp.mt () in
+    System.with_time ~batch ~header (interp_control ~st) (pop_control cl vernac)
 
 let () =
   declare_int_option
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 0968632c2d..84f437f640 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -414,12 +414,17 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_control_r =
-  | VernacExpr of Attributes.vernac_flags * vernac_expr
+type control_flag =
+  | ControlTime of bool
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control
-  | VernacRedirect of string * vernac_control
-  | VernacTimeout of int * vernac_control
-  | VernacFail of vernac_control
+  | ControlRedirect of string
+  | ControlTimeout of int
+  | ControlFail
+
+type vernac_control_r =
+  { control : control_flag list
+  ; attrs : Attributes.vernac_flags
+  ; expr : vernac_expr
+  }
 and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 747998c6cc..903a28e953 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,47 +13,26 @@
 
 open Vernacexpr
 
-let rec under_control v = v |> CAst.with_val (function
-  | VernacExpr (_, c) -> c
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacFail c
-  | VernacTimeout (_,c) -> under_control c
-  )
-
-let rec has_Fail v = v |> CAst.with_val (function
-  | VernacExpr _ -> false
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacTimeout (_,c) -> has_Fail c
-  | VernacFail _ -> true)
+(* Does this vernacular involve Fail? *)
+let has_Fail { CAst.v } = List.mem ControlFail v.control
 
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let is_navigation_vernac_expr = function
+let is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBack _ -> true
   | _ -> false
 
-let is_navigation_vernac c =
-  is_navigation_vernac_expr (under_control c)
-
-let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
-  | VernacTime (_,c) -> is_deep_navigation_vernac c
-  | VernacRedirect (_, c)
-  | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
-  | VernacExpr _ -> false)
-
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = CAst.with_val (function
-  | VernacExpr ( _, VernacResetInitial)
-  | VernacExpr (_, VernacResetName _) -> true
-  | _ -> false)
+let is_reset = function
+  | VernacResetInitial
+  | VernacResetName _ -> true
+  | _ -> false
 
-let is_debug cmd = match under_control cmd with
+let is_debug = function
   | VernacSetOption (_, ["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_undo cmd = match under_control cmd with
+let is_undo = function
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index 8875b86d94..320878e401 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -13,16 +13,9 @@
 
 open Vernacexpr
 
-(* Return the vernacular command below control (Time, Timeout, Redirect, Fail).
-   Beware that Fail can change many properties of the underlying command, since
-   a success of Fail means the command was backtracked over. *)
-val under_control : vernac_control -> vernac_expr
-
 val has_Fail : vernac_control -> bool
-
-val is_navigation_vernac : vernac_control -> bool
-val is_deep_navigation_vernac : vernac_control -> bool
-val is_reset : vernac_control -> bool
-val is_debug : vernac_control -> bool
-val is_undo : vernac_control -> bool
+val is_navigation_vernac : vernac_expr -> bool
+val is_reset : vernac_expr -> bool
+val is_debug : vernac_expr -> bool
+val is_undo : vernac_expr -> bool