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

5 files changed, 139 insertions, 118 deletions

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 :