Separate vernac controls and regular commands.

Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.

23 files changed, 283 insertions, 230 deletions

diff --git a/API/API.mli b/API/API.mli
index a69766901..24a99d57f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4159,10 +4159,6 @@ sig
 
   type vernac_expr =
   | VernacLoad of verbose_flag * string
-  | VernacTime of vernac_expr Loc.located
-  | VernacRedirect of string * vernac_expr Loc.located
-  | VernacTimeout of int * vernac_expr
-  | VernacFail of vernac_expr
   | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of bool * scope_name
   | VernacDelimiters of scope_name * string option
@@ -4294,6 +4290,16 @@ sig
   and vernac_classification = vernac_type * vernac_when
   and one_inductive_expr =
     ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
+
+type vernac_control =
+  | VernacExpr of vernac_expr
+   (* Control *)
+  | VernacTime of vernac_control Loc.located
+  | VernacRedirect of string * vernac_control Loc.located
+  | VernacTimeout of int * vernac_control
+  | VernacFail of vernac_control
+
+
 end
 (* XXX: end of moved from intf *)
 
@@ -5175,9 +5181,7 @@ sig
     val gallina_ext : vernac_expr Gram.entry
     val command : vernac_expr Gram.entry
     val syntax : vernac_expr Gram.entry
-    val vernac : vernac_expr Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val vernac_eoi : vernac_expr Gram.entry
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
@@ -5973,7 +5977,7 @@ end
 
 module Ppvernac :
 sig
-  val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
+  val pr_vernac : Vernacexpr.vernac_control -> Pp.t
   val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
 end
 
@@ -6221,7 +6225,7 @@ sig
   val classify_as_proofstep : Vernacexpr.vernac_classification
   val classify_as_query : Vernacexpr.vernac_classification
   val classify_as_sideeff : Vernacexpr.vernac_classification
-  val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification
+  val classify_vernac : Vernacexpr.vernac_control -> Vernacexpr.vernac_classification
 end
 
 module Stm :
diff --git a/dev/base_include b/dev/base_include
index d7059fe74..4dc9a0bee 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -193,7 +193,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
 let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 58599a14d..aafc3fc59 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -54,7 +54,7 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Universes"];
   ["Printing";"Unfocused"]]
 
-let is_known_option cmd = match cmd with
+let is_known_option cmd = match Vernacprop.under_control cmd with
   | VernacSetOption (o,BoolValue true)
   | VernacUnsetOption o -> coqide_known_option o
   | _ -> false
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index c7a9db1cb..a90e5501a 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -315,13 +315,8 @@ type cumulative_inductive_parsing_flag =
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
-  (* Control *)
-  | VernacLoad of verbose_flag * string
-  | VernacTime of vernac_expr located
-  | VernacRedirect of string * vernac_expr located
-  | VernacTimeout of int * vernac_expr
-  | VernacFail of vernac_expr
 
+  | VernacLoad of verbose_flag * string
   (* Syntax *)
   | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of bool * scope_name
@@ -482,6 +477,14 @@ and vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
+type vernac_control =
+  | VernacExpr of vernac_expr
+   (* Control *)
+  | VernacTime of vernac_control located
+  | VernacRedirect of string * vernac_control located
+  | VernacTimeout of int * vernac_control
+  | VernacFail of vernac_control
+
 (* A vernac classifier provides information about the exectuion of a
    command:
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 444f36833..c18c6810f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -65,14 +65,17 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
       Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
 
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext noedit_mode subprf;
-  vernac: FIRST
+  GLOBAL: vernac_control gallina_ext noedit_mode subprf;
+  vernac_control: FIRST
     [ [ IDENT "Time"; c = located_vernac -> VernacTime c
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
-      | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
-      | IDENT "Fail"; v = vernac -> VernacFail v
-
-      | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
+      | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
+      | IDENT "Fail"; v = vernac_control -> VernacFail v
+      | v = vernac -> VernacExpr(v) ]
+    ]
+  ;
+  vernac:
+    [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
       | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
 
       | v = vernac_poly -> v ]
@@ -111,7 +114,7 @@ GEXTEND Gram
   ;
 
   located_vernac:
-    [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ]
+    [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ]
   ;
 END
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b766f0c6b..c934d38a2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -503,8 +503,7 @@ module Vernac_ =
     let gallina_ext = gec_vernac "gallina_ext"
     let command = gec_vernac "command"
     let syntax = gec_vernac "syntax_command"
-    let vernac = gec_vernac "Vernac.vernac"
-    let vernac_eoi = eoi_entry vernac
+    let vernac_control = gec_vernac "Vernac.vernac_control"
     let rec_definition = gec_vernac "Vernac.rec_definition"
     let red_expr = make_gen_entry utactic "red_expr"
     let hint_info = gec_vernac "hint_info"
@@ -517,7 +516,7 @@ module Vernac_ =
       let act_eoi = Gram.action (fun _ loc -> None) in
       let rule = [
         ([ Symbols.stoken Tok.EOI ], act_eoi);
-        ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
+        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
       ] in
       uncurry (Gram.extend main_entry) (None, make_rule rule)
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3ca013a96..756d9487d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -251,9 +251,8 @@ module Vernac_ :
     val gallina_ext : vernac_expr Gram.entry
     val command : vernac_expr Gram.entry
     val syntax : vernac_expr Gram.entry
-    val vernac : vernac_expr Gram.entry
+    val vernac_control : vernac_control Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val vernac_eoi : vernac_expr Gram.entry
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
@@ -261,7 +260,7 @@ module Vernac_ :
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_expr) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Gram.entry
 
 (** Handling of the proof mode entry *)
 val get_command_entry : unit -> vernac_expr Gram.entry
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 87609296b..2fd6f53c4 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))
+             (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 889c064b2..97066e531 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1509,7 +1509,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1524,7 +1524,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 46ef2ac03..418d4a0b8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -535,16 +535,25 @@ open Decl_kinds
       | SsFwdClose e -> "("^aux e^")*"
     in Pp.str (aux e)
 
-  let rec pr_vernac_body v =
+  let rec pr_vernac_expr v =
     let return = tag_vernac v in
     match v with
       | VernacPolymorphic (poly, v) ->
         let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
-        return (s ++ spc () ++ pr_vernac_body v)
+        return (s ++ spc () ++ pr_vernac_expr v)
       | VernacProgram v ->
-        return (keyword "Program" ++ spc() ++ pr_vernac_body v)
+        return (keyword "Program" ++ spc() ++ pr_vernac_expr v)
       | VernacLocal (local, v) ->
-        return (pr_locality local ++ spc() ++ pr_vernac_body v)
+        return (pr_locality local ++ spc() ++ pr_vernac_expr v)
+
+      | VernacLoad (f,s) ->
+        return (
+          keyword "Load"
+          ++ if f then
+              (spc() ++ keyword "Verbose" ++ spc())
+            else
+              spc() ++ qs s
+        )
 
       (* Proof management *)
       | VernacAbortAll ->
@@ -607,24 +616,6 @@ open Decl_kinds
       | VernacRestoreState s ->
         return  (keyword "Restore State" ++ spc() ++ qs s)
 
-    (* Control *)
-      | VernacLoad (f,s) ->
-        return (
-          keyword "Load"
-          ++ if f then
-              (spc() ++ keyword "Verbose" ++ spc())
-            else
-              spc() ++ qs s
-        )
-      | VernacTime (_,v) ->
-        return (keyword "Time" ++ spc() ++ pr_vernac_body v)
-      | VernacRedirect (s, (_,v)) ->
-        return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v)
-      | VernacTimeout(n,v) ->
-        return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v)
-      | VernacFail v ->
-        return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
-
     (* Syntax *)
       | VernacOpenCloseScope (opening,sc) ->
         return (
@@ -1228,6 +1219,19 @@ open Decl_kinds
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
-  let pr_vernac v =
-    try pr_vernac_body v ++ sep_end v
-    with e -> CErrors.print e
+  let rec pr_vernac_control v =
+    let return = tag_vernac v in
+    match v with
+    | VernacExpr v' -> 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
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index cf27b413c..34b4fb97f 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -12,11 +12,11 @@
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
 
-(** Prints a vernac expression *)
-val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t
+(** Prints a vernac expression without dot *)
+val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t
 
 (** Prints a "proof using X" clause. *)
 val pr_using : Vernacexpr.section_subset_expr -> Pp.t
 
 (** Prints a vernac expression and closes it with a dot. *)
-val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
+val pr_vernac : Vernacexpr.vernac_control -> Pp.t
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 77642946c..01b5b9a01 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
 val unit_val : Stm.DynBlockData.t
 val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
 val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
-val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
-val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
+val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
 
 end = struct
 
@@ -32,7 +32,7 @@ let unit_tag = DynBlockData.create "unit"
 let unit_val = DynBlockData.Easy.inj () unit_tag
 
 let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
-let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
 
 let simple_goal sigma g gs =
   let open Evar in
@@ -74,14 +74,16 @@ include Util
 (* ****************** - foo - bar - baz *********************************** *)
 
 let static_bullet ({ entry_point; prev_node } as view) =
-  match entry_point.ast with
+  assert (not (Vernacprop.has_Fail entry_point.ast));
+  match Vernacprop.under_control entry_point.ast with
   | Vernacexpr.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
-        match node.ast with
+        if Vernacprop.has_Fail node.ast then `Stop
+        else match Vernacprop.under_control node.ast with
         | Vernacexpr.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 }
@@ -94,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+         recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -104,9 +106,10 @@ let () = register_proof_block_delimiter
 (* ******************** { block } ***************************************** *)
   
 let static_curly_brace ({ entry_point; prev_node } as view) =
-  assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+  assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
   crawl view (fun (nesting,prev) node ->
-    match node.ast with
+    if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
+    else match Vernacprop.under_control node.ast with
     | Vernacexpr.VernacSubproof _ when nesting = 0 ->
       `Found { block_stop = entry_point.id; block_start = prev.id;
                dynamic_switch = node.id; carry_on_data = unit_val }
@@ -122,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some Vernacexpr.VernacEndSubproof
+         recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
       }
   | `Not -> `Leaks
 
@@ -164,7 +167,7 @@ let static_indent ({ entry_point; prev_node } as view) =
         else 
           `Found { block_stop = entry_point.id; block_start = node.id;
                    dynamic_switch = node.id;
-                   carry_on_data = of_vernac_expr_val entry_point.ast }
+                   carry_on_data = of_vernac_control_val entry_point.ast }
         ) last_tac
 
 let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
@@ -176,7 +179,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = but_last;
-         recovery_command = Some (to_vernac_expr_val e);
+         recovery_command = Some (to_vernac_control_val e);
       }
   | `Not -> `Leaks
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 1d46e0833..36fc015ef 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -20,6 +20,7 @@ let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else
 
 open Pp
 open CErrors
+open Names
 open Feedback
 open Vernacexpr
 
@@ -111,7 +112,7 @@ type aast = {
   loc : Loc.t option;
   indentation : int;
   strlen : int;
-  mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
+  mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
 }
 let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
 
@@ -119,14 +120,14 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.
 
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
-  | { expr = VernacPrint _ } -> true
-  | { expr = VernacExtend (("Extraction",_), _) } -> true
-  | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
-  | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+  | VernacPrint _
+  | VernacExtend (("Extraction",_), _)
+  | VernacExtend (("SeparateExtraction",_), _)
+  | VernacExtend (("ExtractionLibrary",_), _)
+  | VernacExtend (("RecursiveExtractionLibrary",_), _)
+  | VernacExtend (("ExtractionConstant",_), _)
+  | VernacExtend (("ExtractionInlinedConstant",_), _)
+  | VernacExtend (("ExtractionInductive",_), _) -> true
   | _ -> false
 
 let update_global_env () =
@@ -545,12 +546,10 @@ 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
-    (let rec aux x = match x with
-    | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i
-    | VernacTime (_, e)
-    | VernacTimeout (_, e) -> aux e
-    | _ -> "branch" in aux x)
+    (match Vernacprop.under_control x with
+    | VernacDefinition (_,((_,i),_),_) -> Id.to_string i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i
+    | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
   let get_info id =
@@ -984,7 +983,7 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
   in
   (* Some special handling of bullets and { }, to get a nicer display *)
   let pred n = max 0 (n-1) in
-  let ind, nl, new_beginend = match cmd with
+  let ind, nl, new_beginend = match Vernacprop.under_control cmd with
     | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
     | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
     | VernacBullet _ -> pred ind, nl, beginend
@@ -1049,25 +1048,26 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
   (* We need to check if a command should be filtered from
    * vernac_entries, as it cannot handle it. This should go away in
    * future refactorings.
-   *)
-  let rec is_filtered_command = function
-  | VernacResetName _ | VernacResetInitial | VernacBack _
-  | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
-  | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-  | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
-  | _ -> false
+  *)
+  let is_filtered_command = function
+    | VernacResetName _ | VernacResetInitial | VernacBack _
+    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+    | _ -> false
   in
-  let aux_interp st cmd =
-  if is_filtered_command cmd then
-    (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
-  else match cmd with
-  | VernacShow ShowScript -> ShowScript.show_script (); st
-  | expr ->
-    stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-    try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
-    with e ->
-      let e = CErrors.push e in
-      Exninfo.iraise Hooks.(call_process_error_once e)
+  let aux_interp st expr =
+    let cmd = Vernacprop.under_control expr in
+    if is_filtered_command cmd then
+      (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+    else
+      match cmd with
+      | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
+      | _ ->
+        stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
+        with e ->
+          let e = CErrors.push e in
+          Exninfo.iraise Hooks.(call_process_error_once e)
   in aux_interp st expr
 
 (****************************** CRUFT *****************************************)
@@ -1083,7 +1083,7 @@ module Backtrack : sig
   val branches_of : Stateid.t -> backup
 
   (* Returns the state that the command should backtract to *)
-  val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when
+  val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
 
 end = struct (* {{{ *)
 
@@ -1131,7 +1131,11 @@ end = struct (* {{{ *)
           match VCS.visit id with
           | { step = `Fork ((_,_,_,l),_) } -> l, false,0
           | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
-          | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
+          | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
+          begin match Vernacprop.under_control expr with
+                | VernacUndo n -> [], false, n
+                | _ -> [],false,0
+          end
           | _ -> [],false,0 in
         match f acc (id, vcs, ids, tactic, undo) with
         | `Stop x -> x
@@ -1149,7 +1153,7 @@ end = struct (* {{{ *)
     if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
-      match v with
+      match Vernacprop.under_control v with
       | VernacResetInitial ->
           Stateid.initial, VtNow
       | VernacResetName (_,name) ->
@@ -1242,7 +1246,7 @@ let _ = CErrors.register_handler (function
 
 type document_node = {
   indentation : int;
-  ast : Vernacexpr.vernac_expr;
+  ast : Vernacexpr.vernac_control;
   id : Stateid.t;
 }
 
@@ -1257,7 +1261,7 @@ type static_block_detection =
 type recovery_action = {
   base_state : Stateid.t;
   goals_to_admit : Goal.goal list;
-  recovery_command : Vernacexpr.vernac_expr option;
+  recovery_command : Vernacexpr.vernac_control option;
 }
 
 type dynamic_block_error_recovery =
@@ -1494,7 +1498,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = (VernacEndProof (Proved (Opaque,None))) }) in
+              expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1642,7 +1646,7 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = (VernacEndProof (Proved (Opaque,None))) });
+          expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) });
       `OK proof
       end
     with e ->
@@ -2107,30 +2111,43 @@ let collect_proof keep cur hd brkind id =
    | [] -> no_name
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).loc in
- let rec is_defined_expr = function
+ let is_defined_expr = function
    | VernacEndProof (Proved (Transparent,_)) -> true
-   | VernacTime (_, e) -> is_defined_expr e
-   | VernacRedirect (_, (_, e)) -> is_defined_expr e
-   | VernacTimeout (_, e) -> is_defined_expr e
    | _ -> false in
  let is_defined = function
-   | _, { expr = e } -> is_defined_expr e in
+   | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+                        && (not (Vernacprop.has_Fail e)) in
+ let proof_using_ast = function
+   | VernacProof(_,Some _) -> true
+   | _ -> false
+ in
  let proof_using_ast = function
-   | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
+   | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+                      && (not (Vernacprop.has_Fail v.expr)) -> Some v
    | _ -> None in
  let has_proof_using x = proof_using_ast x <> None in
  let proof_no_using = function
-   | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v
+   | VernacProof(t,None) -> t
+   | _ -> assert false
+ in
+ let proof_no_using = function
+   | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
    | _ -> assert false in
  let has_proof_no_using = function
-   | Some (_, { expr = VernacProof(_,None) }) -> true
+   | VernacProof(_,None) -> true
+   | _ -> false
+ in
+ let has_proof_no_using = function
+   | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+                    && (not (Vernacprop.has_Fail v.expr))
    | _ -> false in
  let too_complex_to_delegate = function
-   | { expr = (VernacDeclareModule _
-              | VernacDefineModule _
-              | VernacDeclareModuleType _
-              | VernacInclude _) } -> true
-   | { expr =  (VernacRequire _ | VernacImport _) } -> true
+   | VernacDeclareModule _
+   | VernacDefineModule _
+   | VernacDeclareModuleType _
+   | VernacInclude _
+   | VernacRequire _
+   | VernacImport _ -> true
    | ast -> may_pierce_opaque ast in
  let parent = function Some (p, _) -> p | None -> assert false in
  let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
@@ -2138,7 +2155,8 @@ 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 x -> `Sync(no_name,`Print)
+      when too_complex_to_delegate (Vernacprop.under_control x.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
     (* An Alias could jump everywhere... we hope we can ignore it*)
@@ -2158,7 +2176,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 <- VernacProof(t, Some hint);
+          v.expr <- VernacExpr(VernacProof(t, Some hint));
           `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
@@ -2177,9 +2195,13 @@ let collect_proof keep cur hd brkind id =
    | `ASync(_,_,name,_) -> `Sync (name,why) in
 
  let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
+ let is_vernac_exact = function
+   | VernacExactProof _ -> true
+   | _ -> false
+ in
  match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _
- | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
+ | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+                                && (not (Vernacprop.has_Fail x.expr)) ->
      `Sync (no_name,`Immediate)
  | _, _, { VCS.kind = `Edit _ }  -> check_policy (collect (Some cur) [] id)
  | _ ->
@@ -2752,7 +2774,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
             if !async_proofs_full then `QueryQueue (ref false)
             else if VCS.is_vio_doc () &&
                     VCS.((get_branch head).kind = `Master) &&
-                    may_pierce_opaque x
+                    may_pierce_opaque (Vernacprop.under_control x.expr)
                  then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
@@ -2814,7 +2836,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
           rc
 
       (* Side effect on all branches *)
-      | VtUnknown, _ when expr = VernacToplevelControl Drop ->
+      | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop ->
         let st = Vernacstate.freeze_interp_state `No in
         ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
         `Ok
@@ -2826,7 +2848,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
           VCS.commit id (mkTransCmd x l in_proof `MainQueue);
           (* We can't replay a Definition since universes may be differently
            * inferred.  This holds in Coq >= 8.5 *)
-	  let action = match x.expr with
+          let action = match Vernacprop.under_control x.expr with
 	    | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
 	    | _ -> ReplayCommand x in
 	  VCS.propagate_sideff ~action;
@@ -2854,7 +2876,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
                 | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
                 | VernacLocal (_,e) -> opacity_of_produced_term e
                 | _ -> Doesn'tGuaranteeOpacity in
-              VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
               let proof_mode = default_proof_mode () in
               VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
diff --git a/stm/stm.mli b/stm/stm.mli
index ef95be0e4..587b75642 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -39,7 +39,7 @@ val new_doc  : stm_init_options -> doc * Stateid.t
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
 val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
-  Vernacexpr.vernac_expr Loc.located
+  Vernacexpr.vernac_control Loc.located
 
 (* Reminder: A parsable [pa] is constructed using
    [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
@@ -53,7 +53,7 @@ exception End_of_input
    If [newtip] is provided, then the returned state id is guaranteed
    to be [newtip] *)
 val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
-  bool -> Vernacexpr.vernac_expr Loc.located ->
+  bool -> Vernacexpr.vernac_control Loc.located ->
   doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
@@ -111,7 +111,7 @@ val get_current_state : doc:doc -> Stateid.t
 val get_ldir : doc:doc -> Names.DirPath.t
 
 (* This returns the node at that position *)
-val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
@@ -174,7 +174,7 @@ type static_block_declaration = {
 
 type document_node = {
   indentation : int;
-  ast : Vernacexpr.vernac_expr;
+  ast : Vernacexpr.vernac_control;
   id : Stateid.t;
 }
 
@@ -189,7 +189,7 @@ type static_block_detection =
 type recovery_action = {
   base_state : Stateid.t;
   goals_to_admit : Goal.goal list;
-  recovery_command : Vernacexpr.vernac_expr option;
+  recovery_command : Vernacexpr.vernac_control option;
 }
 
 type dynamic_block_error_recovery =
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5ae27a11..1291b7642 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -8,6 +8,7 @@
 
 open Vernacexpr
 open CErrors
+open Util
 open Pp
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
@@ -47,36 +48,18 @@ let declare_vernac_classifier
 =
   classifiers := !classifiers @ [s,f]
 
-let make_polymorphic (a, b as x) =
-  match a with
-  | VtStartProof (x, _, ids) ->
-      VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
-  | _ -> x
-
-let rec classify_vernac e =
-  let static_classifier e = match e with
+let classify_vernac e =
+  let rec static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
-    | VernacSetOption (["Universe"; "Polymorphism"],_)
-    | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
+    | ( VernacSetOption (l,_) | VernacUnsetOption l)
+      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+       VtSideff [], VtNow
     (* Nested vernac exprs *)
-    | VernacProgram e -> classify_vernac e
-    | VernacLocal (_,e) -> classify_vernac e
-    | VernacPolymorphic (b, e) -> 
-      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
-	make_polymorphic (classify_vernac e)
-      else classify_vernac e
-    | VernacTimeout (_,e) -> classify_vernac 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 _
-          | VtProofMode _ | VtMeta), _ as x -> x
-        | VtQed _, _ ->
-            VtProofStep { parallel = `No; proof_block_detection = None },
-            VtNow
-        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+    | VernacProgram e -> static_classifier ~poly e
+    | VernacLocal (_,e) -> static_classifier ~poly e
+    | VernacPolymorphic (b, e) -> static_classifier ~poly:b e
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
@@ -106,17 +89,20 @@ let rec classify_vernac e =
     | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
-        VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof(default_proof_mode (),guarantee,[i]), VtLater
     | VernacStartTheoremProof (_,l) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
-        VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+    | VernacGoal _ ->
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+       VtStartProof (default_proof_mode (),guarantee,[]), VtLater
     | VernacFixpoint (discharge,l) ->
        let guarantee =
-         match discharge with
-         | Decl_kinds.NoDischarge -> GuaranteesOpacity
-         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
        in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
@@ -126,9 +112,8 @@ let rec classify_vernac e =
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
        let guarantee =
-         match discharge with
-         | Decl_kinds.NoDischarge -> GuaranteesOpacity
-         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
        in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
@@ -207,10 +192,21 @@ let rec classify_vernac e =
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let res = static_classifier e in
-    if Flags.is_universe_polymorphism () then
-      make_polymorphic res
-    else res
+  let rec static_control_classifier ~poly = function
+    | VernacExpr e -> static_classifier ~poly e
+    | VernacTimeout (_,e) -> static_control_classifier ~poly e
+    | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+       static_control_classifier ~poly e
+    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+        (match static_control_classifier ~poly e with
+        | ( VtQuery _ | VtProofStep _ | VtSideff _
+          | VtProofMode _ | VtMeta), _ as x -> x
+        | VtQed _, _ ->
+            VtProofStep { parallel = `No; proof_block_detection = None },
+            VtNow
+        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+  in
+  static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
 let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
 let classify_as_sideeff = VtSideff [], VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index fe42a03a3..c0571c1d6 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -12,7 +12,7 @@ open Genarg
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
-val classify_vernac : vernac_expr -> vernac_classification
+val classify_vernac : vernac_control -> vernac_classification
 
 (** Install a vernacular classifier for VernacExtend *)
 val declare_vernac_classifier :
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8fdaedbaf..24d414c88 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -111,13 +111,14 @@ let pr_open_cur_subgoals () =
 (*   | _ -> false *)
 
 let rec interp_vernac ~check ~interactive doc sid (loc,com) =
-  let interp = function
+  let interp v =
+    match under_control v with
     | VernacLoad (verbosely, fname) ->
-	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
+        let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
         load_vernac ~verbosely ~check ~interactive doc sid f
-    | v ->
+    | _ ->
 
       (* XXX: We need to run this before add as the classification is
          highly dynamic and depends on the structure of the
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index f9a430026..8a798a98e 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,7 +12,7 @@
     expected to handle and print errors in form of exceptions, however
     care is taken so the state machine is left in a consistent
     state. *)
-val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t
+val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 6c3dfec7d..1bb9e0da1 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -80,8 +80,8 @@ let pr_grammar = function
   | "pattern" ->
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->
-      str "Entry vernac is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.vernac ++
+      str "Entry vernac_control is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.vernac_control ++
       str "Entry command is" ++ fnl () ++
       pr_entry Pcoq.Vernac_.command ++
       str "Entry syntax is" ++ fnl () ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a581043ac..aa6121c39 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1380,11 +1380,13 @@ let _ =
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
+let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
+
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "universe polymorphism";
-      optkey   = ["Universe"; "Polymorphism"];
+      optkey   = universe_polymorphism_option_name;
       optread  = Flags.is_universe_polymorphism;
       optwrite = Flags.make_universe_polymorphism }
 
@@ -1933,19 +1935,11 @@ let vernac_load interp fname =
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
   let open Vernacinterp in
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
-  (* The below vernac are candidates for removal from the main type
-     and to be put into a new doc_command datatype: *)
 
   | VernacLoad _ -> assert false
 
-  (* Done later in this file *)
-  | VernacFail _ -> assert false
-  | VernacTime _ -> assert false
-  | VernacRedirect _ -> assert false
-  | VernacTimeout _ -> assert false
-
   (* The STM should handle that, but LOAD bypasses the STM... *)
   | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
   | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
@@ -2209,7 +2203,20 @@ let with_fail st b f =
 
 let interp ?(verbosely=true) ?proof ~st (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
-  let rec aux ?polymorphism ~atts isprogcmd = function
+  let rec control = function
+  | VernacExpr v ->
+      let atts = { loc; locality = None; polymorphic = false; } in
+      aux ~atts orig_program_mode v
+  | VernacFail v -> with_fail st true (fun () -> control v)
+  | VernacTimeout (n,v) ->
+      current_timeout := Some n;
+      control v
+  | VernacRedirect (s, (_,v)) ->
+       Topfmt.with_output_to_file s control v
+  | VernacTime (_,v) ->
+      System.with_time !Flags.time control v;
+
+  and aux ?polymorphism ~atts isprogcmd = function
 
     | VernacProgram c when not isprogcmd ->
       aux ?polymorphism ~atts true c
@@ -2229,20 +2236,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
     | VernacLocal _ ->
       user_err Pp.(str "Locality specified twice")
 
-    | VernacFail v ->
-      with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v)
-
-    | VernacTimeout (n,v) ->
-      current_timeout := Some n;
-      aux ?polymorphism ~atts isprogcmd v
-
-    | VernacRedirect (s, (_,v)) ->
-      Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v
-
-    | VernacTime (_,v) ->
-      System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v;
-
-    | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname
+    | VernacLoad (_,fname) -> vernac_load control fname
 
     | c ->
       check_vernac_supports_locality c atts.locality;
@@ -2272,10 +2266,9 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
 	    ignore (Flags.use_polymorphic_flag ());
             iraise e
   in
-  let atts = { loc; locality = None; polymorphic = false; } in
   if verbosely
-  then Flags.verbosely (aux ~atts orig_program_mode) c
-  else aux ~atts orig_program_mode c
+  then Flags.verbosely control c
+  else control  c
 
 (* XXX: There is a bug here in case of an exception, see @gares
    comments on the PR *)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a559912a0..e99a62fe6 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-  st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
+  st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -36,3 +36,5 @@ val command_focus : unit Proof.focus_kind
 
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
+
+val universe_polymorphism_option_name : string list
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3cff1f14c..4a01ef2ef 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -11,32 +11,49 @@
 
 open Vernacexpr
 
+let rec under_control = function
+  | VernacExpr c -> c
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+
+let rec has_Fail = function
+  | VernacExpr c -> false
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacTimeout (_,c) -> has_Fail c
+  | VernacFail _ -> true
+
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let rec is_navigation_vernac = function
+let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, (_,c))
-  | VernacTime (_,c) ->
-      is_navigation_vernac c (* Time Back* is harmless *)
-  | c -> is_deep_navigation_vernac c
+  | _ -> false
 
-and is_deep_navigation_vernac = function
+let is_navigation_vernac c =
+  is_navigation_vernac_expr (under_control c)
+
+let rec is_deep_navigation_vernac = function
+  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacRedirect (_, (_,c))
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | _ -> false
+  | VernacExpr _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
 let is_reset = function
-  | VernacResetInitial | VernacResetName _ -> true
+  | VernacExpr VernacResetInitial
+  | VernacExpr (VernacResetName _) -> true
   | _ -> false
 
-let is_debug cmd = match cmd with
+let is_debug cmd = match under_control cmd with
   | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_query cmd = match cmd with
+let is_query cmd = match under_control cmd with
   | VernacChdir None
   | VernacMemOption _
   | VernacPrintOption _
@@ -47,6 +64,6 @@ let is_query cmd = match cmd with
   | VernacLocate _ -> true
   | _ -> false
 
-let is_undo cmd = match cmd with
+let is_undo cmd = match under_control cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index fbdba6bac..eb7c7055a 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -11,9 +11,16 @@
 
 open Vernacexpr
 
-val is_navigation_vernac : vernac_expr -> bool
-val is_deep_navigation_vernac : vernac_expr -> bool
-val is_reset : vernac_expr -> bool
-val is_query : vernac_expr -> bool
-val is_debug : vernac_expr -> bool
-val is_undo : vernac_expr -> bool
+(* 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_query : vernac_control -> bool
+val is_debug : vernac_control -> bool
+val is_undo : vernac_control -> bool