Merge PR #6318: Separate vernac controls and regular commands.

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 3cb6bd9b6..afb6fabcb 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