[vernac] Interpret regular vernacs symbolically

This provides uniformity to the inner loop and prepares the way to
export a refined type for interpretation.

The only non-uniformity remaining is the one due to the `?proof`
parameter; it won't be easy to fix due to upper layers issues.

Note that this step is not yet fully satisfying, as a true typed
`vernac_expr` definition is still not possible because of syntactic
non-uniformity, in particular all the surgery done for `CoFixpoint`
and `Instance` should be eliminated in favor of more refined AST tags.

An interesting TODO is to handle attributes symbolically too, as to
remove boilerplate.

5 files changed, 338 insertions, 332 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d0ec575eb3..d14c7ddf8f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -207,12 +207,8 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
-let fresh_name_for_anonymous_theorem ~pstate =
-  let avoid = match pstate with
-  | None -> Id.Set.empty
-  | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate)
-  in
-  next_global_ident_away default_thm_id avoid
+let fresh_name_for_anonymous_theorem () =
+  next_global_ident_away default_thm_id Id.Set.empty
 
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index c4c609e824..3df543156d 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -61,7 +61,7 @@ val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
   Proof_global.proof_terminator
 
-val fresh_name_for_anonymous_theorem : pstate:Proof_global.stack option -> Id.t
+val fresh_name_for_anonymous_theorem : unit -> Id.t
 
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca4b50318b..18e0fde296 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -47,10 +47,7 @@ let vernac_pperr_endline pp =
 let there_are_pending_proofs ~pstate =
   not Option.(is_empty pstate)
 
-let check_no_pending_proof ~pstate =
-  if there_are_pending_proofs ~pstate then
-    user_err Pp.(str "Command not supported (Open proofs remain)")
-
+(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *)
 let vernac_require_open_proof ~pstate f =
   match pstate with
   | Some pstate -> f ~pstate
@@ -60,19 +57,9 @@ let with_pstate ~pstate f =
   vernac_require_open_proof ~pstate
     (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
 
-let modify_pstate ~pstate f =
-  vernac_require_open_proof ~pstate (fun ~pstate ->
-      Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
-
-let with_read_proof ~pstate f =
-  f ~pstate;
-  pstate
-
-let with_open_proof ~pstate f =
-  Some (Proof_global.push ~ontop:pstate (f ~pstate))
-
-let with_open_proof_simple ~pstate f =
-  Some (Proof_global.push ~ontop:pstate f)
+ let modify_pstate ~pstate f =
+   vernac_require_open_proof ~pstate (fun ~pstate ->
+       Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
 
 let get_current_or_global_context ~pstate =
   match pstate with
@@ -610,10 +597,11 @@ let vernac_definition_hook p = function
   Some (Class.add_subclass_hook p)
 | _ -> None
 
-let vernac_definition_name lid local ~pstate =
+let vernac_definition_name lid local =
   let lid =
     match lid with
-    | { v = Name.Anonymous; loc } -> CAst.make ?loc (fresh_name_for_anonymous_theorem ~pstate)
+    | { v = Name.Anonymous; loc } ->
+         CAst.make ?loc (fresh_name_for_anonymous_theorem ())
     | { v = Name.Name n; loc } -> CAst.make ?loc n in
   let () =
     match local with
@@ -622,25 +610,25 @@ let vernac_definition_name lid local ~pstate =
   in
   lid
 
-let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t ~pstate =
+let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let program_mode = atts.program in
-  let name = vernac_definition_name lid local ~pstate in
+  let name = vernac_definition_name lid local in
   start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
 
-let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt ~pstate =
+let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let program_mode = atts.program in
-  let name = vernac_definition_name lid local ~pstate in
-  let pstate = Option.map Proof_global.get_current_pstate pstate in
+  let name = vernac_definition_name lid local in
   let red_option = match red_option with
     | None -> None
     | Some r ->
-      let sigma, env = get_current_or_global_context ~pstate in
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
   ComDefinition.do_definition ~program_mode name.v
     (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook
@@ -660,13 +648,12 @@ let vernac_end_proof ?pstate:ontop ?proof = function
   | Proved (opaque,idopt) ->
     save_proof_proved ?ontop ?proof ~opaque ~idopt
 
-let vernac_exact_proof ~pstate:ontop c =
+let vernac_exact_proof ~pstate c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
-  let pstate, status = Pfedit.by (Tactics.exact_proof c) (Proof_global.get_current_pstate ontop) in
+  let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
   let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
-  if not status then Feedback.feedback Feedback.AddedAxiom;
-  Proof_global.discard_current ontop
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
@@ -939,14 +926,13 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
 
-let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
+let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
-       check_no_pending_proof ~pstate;
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -986,13 +972,12 @@ let vernac_end_module export {loc;v=id} =
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
 
-let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
 
   match mty_ast_l with
     | [] ->
-       check_no_pending_proof ~pstate;
        let binders_ast,argsexport =
 	 List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -1039,8 +1024,7 @@ let vernac_include l =
 
 (* Sections *)
 
-let vernac_begin_section ~pstate ({v=id} as lid) =
-  check_no_pending_proof ~pstate;
+let vernac_begin_section ({v=id} as lid) =
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
@@ -1053,8 +1037,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
 
 (* Dispatcher of the "End" command *)
 
-let vernac_end_segment ~pstate ({v=id} as lid) =
-  check_no_pending_proof ~pstate;
+let vernac_end_segment ({v=id} as lid) =
   match Lib.find_opening_node id with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1114,25 +1097,34 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~pstate ~atts name bl t props info =
+let vernac_instance_program ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
   let (program, locality), polymorphic =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  if program then begin
-    let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
-    pstate
-  end else begin
-    match props with
-    | None ->
-      with_open_proof_simple ~pstate
-        (let _id, pstate = Classes.new_instance_interactive ~global polymorphic name bl t info in
-         pstate)
-    | Some props ->
-      let _id : Id.t = Classes.new_instance ~global polymorphic name bl t props info in
-      pstate
-  end
+  let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
+  ()
+
+let vernac_instance_interactive ~atts name bl t info =
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  let _id, pstate =
+    Classes.new_instance_interactive ~global polymorphic name bl t info in
+  pstate
+
+let vernac_instance ~atts name bl t props info =
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  let _id : Id.t =
+    Classes.new_instance ~global polymorphic name bl t props info in
+  ()
 
 let vernac_declare_instance ~atts id bl inst pri =
   Dumpglob.dump_definition (fst id) false "inst";
@@ -1898,7 +1890,6 @@ let query_command_selector ?loc = function
       (str "Query commands only support the single numbered goal selector.")
 
 let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
-  let pstate = Option.map Proof_global.get_current_pstate pstate in
   let glopt = query_command_selector glopt in
   let sigma, env = get_current_context_of_args ~pstate glopt in
   let sigma, c = interp_open_constr env sigma rc in
@@ -1998,8 +1989,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let sigma, env = get_current_or_global_context ~pstate in
     print_about env sigma ref_or_by_not udecl
 
-let vernac_print ~(pstate : Proof_global.stack option) ~atts =
-  let pstate = Option.map Proof_global.get_current_pstate pstate in
+let vernac_print ~pstate ~atts =
   let sigma, env = get_current_or_global_context ~pstate in
   function
   | PrintTables -> print_tables ()
@@ -2111,7 +2101,6 @@ let () =
       optwrite = (:=) search_output_name_only }
 
 let vernac_search ~pstate ~atts s gopt r =
-  let pstate = Option.map Proof_global.get_current_pstate pstate in
   let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
   let env,gopt =
@@ -2149,7 +2138,6 @@ let vernac_locate ~pstate = function
   | LocateTerm {v=AN qid} -> print_located_term qid
   | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
-    let pstate = Option.map Proof_global.get_current_pstate pstate in
     let _, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
       (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
@@ -2158,10 +2146,8 @@ let vernac_locate ~pstate = function
   | LocateOther (s, qid) -> print_located_other s qid
   | LocateFile f -> locate_file f
 
-let vernac_register ~pstate qid r =
+let vernac_register qid r =
   let gr = Smartlocate.global_with_alias qid in
-  if there_are_pending_proofs ~pstate then
-    user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   match r with
   | RegisterInline ->
     begin match gr with
@@ -2189,23 +2175,24 @@ let vernac_register ~pstate qid r =
 (********************)
 (* Proof management *)
 
-let vernac_focus gln =
-  Proof_global.simple_with_current_proof (fun _ p ->
+let vernac_focus ~pstate gln =
+  Proof_global.modify_proof (fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
          user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.")
       | Some n ->
          Proof.focus focus_command_cond () n p)
+    pstate
 
   (* Unfocuses one step in the focus stack. *)
-let vernac_unfocus () =
-  Proof_global.simple_with_current_proof
-    (fun _ p -> Proof.unfocus command_focus p ())
+let vernac_unfocus ~pstate =
+  Proof_global.modify_proof
+    (fun p -> Proof.unfocus command_focus p ())
+    pstate
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
-  let pstate = Proof_global.get_current_pstate pstate in
   let p = Proof_global.give_me_the_proof pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
@@ -2219,25 +2206,29 @@ let vernac_unfocused ~pstate =
 let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
-let vernac_subproof gln =
-  Proof_global.simple_with_current_proof (fun _ p ->
+let vernac_subproof gln ~pstate =
+  Proof_global.modify_proof (fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
     | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
     | _ -> user_err ~hdr:"bracket_selector"
              (str "Brackets do not support multi-goal selectors."))
+    pstate
 
-let vernac_end_subproof () =
-  Proof_global.simple_with_current_proof (fun _ p ->
-    Proof.unfocus subproof_kind p ())
+let vernac_end_subproof ~pstate =
+  Proof_global.modify_proof (fun p ->
+      Proof.unfocus subproof_kind p ())
+    pstate
 
-let vernac_bullet (bullet : Proof_bullet.t) =
-  Proof_global.simple_with_current_proof (fun _ p ->
-    Proof_bullet.put p bullet)
+let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
+  Proof_global.modify_proof (fun p ->
+    Proof_bullet.put p bullet) pstate
 
-let vernac_show ~pstate:ontop =
-  match ontop with
+(* Stack is needed due to show proof names, should deprecate / remove
+   and take pstate *)
+let vernac_show ~pstate =
+  match pstate with
   (* Show functions that don't require a proof state *)
   | None ->
     begin function
@@ -2247,8 +2238,7 @@ let vernac_show ~pstate:ontop =
         user_err (str "This command requires an open proof.")
     end
   (* Show functions that require a proof state *)
-  | Some ontop ->
-    let pstate = Proof_global.get_current_pstate ontop in
+  | Some pstate ->
     begin function
     | ShowGoal goalref ->
       let proof = Proof_global.give_me_the_proof pstate in
@@ -2260,7 +2250,7 @@ let vernac_show ~pstate:ontop =
     | ShowExistentials -> show_top_evars ~pstate
     | ShowUniverses -> show_universes ~pstate
     | ShowProofNames ->
-      pr_sequence Id.print (Proof_global.get_all_proof_names ontop)
+      Id.print (Proof_global.get_current_proof_name pstate)
     | ShowIntros all -> show_intro ~pstate all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
@@ -2332,11 +2322,16 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
-let vernac_interp_phase c ~pstate =
+let interp_typed_vernac c ~pstate =
   let open Proof_global in
   let open Vernacextend in
   match c with
   | VtDefault f -> f (); pstate
+  | VtNoProof f ->
+    if there_are_pending_proofs ~pstate then
+      user_err Pp.(str "Command not supported (Open proofs remain)");
+    let () = f () in
+    pstate
   | VtCloseProof f ->
     vernac_require_open_proof ~pstate (fun ~pstate ->
         f ~pstate:(Proof_global.get_current_pstate pstate);
@@ -2352,350 +2347,363 @@ let vernac_interp_phase c ~pstate =
     with_pstate ~pstate f;
     pstate
 
-(* "locality" is the prefix "Local" attribute, while the "local" component
- * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility.
- * loc is the Loc.t of the vernacular command being interpreted. *)
-let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
-  let pstate = st.Vernacstate.proof in
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
-  match c with
-
-  (* 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")
-  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
-
-  (* Resetting *)
-  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
-  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
-  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
-  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
-
-  (* This one is possible to handle here *)
-  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
-
-  (* Loading a file requires access to the control interpreter so
-     [vernac_load] is mutually-recursive with [interp_expr] *)
-  | VernacLoad (verbosely,fname) ->
-    unsupported_attributes atts;
-    vernac_load ?proof ~verbosely ~st fname
-
+(* We interpret vernacular commands to a DSL that specifies their
+   allowed actions on proof states *)
+let translate_vernac ~atts v = let open Vernacextend in match v with
+  | VernacEndProof _
+  | VernacAbortAll
+  | VernacRestart
+  | VernacUndo _
+  | VernacUndoTo _
+  | VernacResetName _
+  | VernacResetInitial
+  | VernacBack _
+  | VernacBackTo _
+  | VernacAbort _
+  | VernacLoad _ ->
+    anomaly (str "type_vernac")
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-    with_module_locality ~atts vernac_syntax_extension infix sl;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl)
   | VernacDeclareScope sc ->
-    with_module_locality ~atts vernac_declare_scope sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_declare_scope sc)
   | VernacDelimiters (sc,lr) ->
-    with_module_locality ~atts vernac_delimiters sc lr;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_delimiters sc lr)
   | VernacBindScope (sc,rl) ->
-    with_module_locality ~atts vernac_bind_scope sc rl;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_bind_scope sc rl)
   | VernacOpenCloseScope (b, s) ->
-    with_section_locality ~atts vernac_open_close_scope (b,s);
-    pstate
+    VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
   | VernacInfix (mv,qid,sc) ->
-    with_module_locality ~atts vernac_infix mv qid sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
   | VernacNotation (c,infpl,sc) ->
-    with_module_locality ~atts vernac_notation c infpl sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
   | VernacNotationAddFormat(n,k,v) ->
-    unsupported_attributes atts;
-    Metasyntax.add_notation_extra_printing_rule n k v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Metasyntax.add_notation_extra_printing_rule n k v)
   | VernacDeclareCustomEntry s ->
-    with_module_locality ~atts vernac_custom_entry s;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_custom_entry s)
 
   (* Gallina *)
-  | VernacDefinition (dk,lid,ProveBody(bl,t)) ->
-    with_open_proof ~pstate (with_def_attributes ~atts vernac_definition_interactive dk lid bl t)
-  | VernacDefinition (dk,lid,DefineBody(bl,red_option,c,typ_opt)) ->
-    with_read_proof ~pstate (with_def_attributes ~atts vernac_definition dk lid bl red_option c typ_opt)
+
+  | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) ->
+    VtDefault (fun () ->
+      with_def_attributes ~atts
+       vernac_definition discharge lid bl red_option c typ)
+  | VernacDefinition (discharge,lid,ProveBody(bl,typ)) ->
+    VtOpenProof(fun () ->
+      with_def_attributes ~atts
+       vernac_definition_interactive discharge lid bl typ)
+
   | VernacStartTheoremProof (k,l) ->
-    with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_start_proof k l)
-  | VernacEndProof e ->
-    unsupported_attributes atts;
-    vernac_end_proof ?proof ?pstate e
+    VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l)
   | VernacExactProof c ->
-    unsupported_attributes atts;
-    vernac_require_open_proof ~pstate (vernac_exact_proof c)
+    VtCloseProof(fun ~pstate ->
+        unsupported_attributes atts;
+        vernac_exact_proof ~pstate c)
+
+  | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
+    let i () =
+      unsupported_attributes atts;
+      vernac_define_module export lid bl mtys mexprl in
+    (* XXX: We should investigate if eventually this should be made
+       VtNoProof in all cases. *)
+    if List.is_empty mexprl then VtNoProof i else VtDefault i
+
+  | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_declare_module_type lid bl mtys mtyo)
   | VernacAssumption ((discharge,kind),nl,l) ->
-    with_def_attributes ~atts vernac_assumption discharge kind l nl;
-    pstate
+    VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl)
   | VernacInductive (cum, priv, finite, l) ->
-    vernac_inductive ~atts cum priv finite l;
-    pstate
+    VtDefault(fun () -> vernac_inductive ~atts cum priv finite l)
   | VernacFixpoint (discharge, l) ->
     let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in
     if opens then
-      with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
+      VtOpenProof (fun () ->
+        with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
     else
-      (with_def_attributes ~atts vernac_fixpoint discharge l; pstate)
+      VtDefault (fun () ->
+        with_def_attributes ~atts vernac_fixpoint discharge l)
   | VernacCoFixpoint (discharge, l) ->
     let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in
     if opens then
-      with_open_proof_simple ~pstate (with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
+      VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
     else
-      (with_def_attributes ~atts vernac_cofixpoint discharge l; pstate)
+      VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l)
+
   | VernacScheme l ->
-    unsupported_attributes atts;
-    vernac_scheme l;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_scheme l)
   | VernacCombinedScheme (id, l) ->
-    unsupported_attributes atts;
-    vernac_combined_scheme id l;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_combined_scheme id l)
   | VernacUniverse l ->
-    vernac_universe ~poly:(only_polymorphism atts) l;
-    pstate
+    VtDefault(fun () -> vernac_universe ~poly:(only_polymorphism atts) l)
   | VernacConstraint l ->
-    vernac_constraint ~poly:(only_polymorphism atts) l;
-    pstate
+    VtDefault(fun () -> vernac_constraint ~poly:(only_polymorphism atts) l)
 
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
-    unsupported_attributes atts;
-    vernac_declare_module export lid bl mtyo;
-    pstate
-  | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
-    unsupported_attributes atts;
-    vernac_define_module ~pstate export lid bl mtys mexprl;
-    pstate
-  | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
-    unsupported_attributes atts;
-    vernac_declare_module_type ~pstate lid bl mtys mtyo;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_declare_module export lid bl mtyo)
   | VernacInclude in_asts ->
-    unsupported_attributes atts;
-    vernac_include in_asts;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_include in_asts)
   (* Gallina extensions *)
   | VernacBeginSection lid ->
-    unsupported_attributes atts;
-    vernac_begin_section ~pstate lid;
-    pstate
-
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_begin_section lid)
   | VernacEndSegment lid ->
-    unsupported_attributes atts;
-    vernac_end_segment ~pstate lid;
-    pstate
-
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_end_segment lid)
   | VernacNameSectionHypSet (lid, set) ->
-    unsupported_attributes atts;
-    vernac_name_sec_hyp lid set;
-    pstate
-
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_name_sec_hyp lid set)
   | VernacRequire (from, export, qidl) ->
-    unsupported_attributes atts;
-    vernac_require from export qidl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_require from export qidl)
   | VernacImport (export,qidl) ->
-    unsupported_attributes atts;
-    vernac_import export qidl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_import export qidl)
   | VernacCanonical qid ->
-    unsupported_attributes atts;
-    vernac_canonical qid;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_canonical qid)
   | VernacCoercion (r,s,t) ->
-    vernac_coercion ~atts r s t;
-    pstate
+    VtDefault(fun () -> vernac_coercion ~atts r s t)
   | VernacIdentityCoercion ({v=id},s,t) ->
-    vernac_identity_coercion ~atts id s t;
-    pstate
+    VtDefault(fun () -> vernac_identity_coercion ~atts id s t)
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    vernac_instance ~pstate ~atts name bl t props info
+    let { DefAttributes.program } = DefAttributes.parse atts in
+    if program then
+      VtDefault (fun () -> vernac_instance_program ~atts name bl t props info)
+    else begin match props with
+    | None ->
+       VtOpenProof(fun () ->
+        vernac_instance_interactive ~atts name bl t info)
+    | Some props ->
+       VtDefault(fun () ->
+        vernac_instance ~atts name bl t props info)
+    end
+
   | VernacDeclareInstance (id, bl, inst, info) ->
-    vernac_declare_instance ~atts id bl inst info;
-    pstate
+    VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info)
   | VernacContext sup ->
-    let () = vernac_context ~poly:(only_polymorphism atts) sup in
-    pstate
+    VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup)
   | VernacExistingInstance insts ->
-    with_section_locality ~atts vernac_existing_instance insts;
-    pstate
+    VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts)
   | VernacExistingClass id ->
-    unsupported_attributes atts;
-    vernac_existing_class id;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_existing_class id)
 
   (* Solving *)
   | VernacSolveExistential (n,c) ->
-    unsupported_attributes atts;
-    modify_pstate ~pstate (vernac_solve_existential n c)
-
+    VtModifyProof(fun ~pstate ->
+        unsupported_attributes atts;
+        vernac_solve_existential ~pstate n c)
   (* Auxiliary file and library management *)
   | VernacAddLoadPath (isrec,s,alias) ->
-    unsupported_attributes atts;
-    vernac_add_loadpath isrec s alias;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_loadpath isrec s alias)
   | VernacRemoveLoadPath s ->
-    unsupported_attributes atts;
-    vernac_remove_loadpath s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_remove_loadpath s)
   | VernacAddMLPath (isrec,s) ->
-    unsupported_attributes atts;
-    vernac_add_ml_path isrec s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_ml_path isrec s)
   | VernacDeclareMLModule l ->
-    with_locality ~atts vernac_declare_ml_module l;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
   | VernacChdir s ->
-    unsupported_attributes atts;
-    vernac_chdir s;
-    pstate
+    VtDefault(fun () -> unsupported_attributes atts; vernac_chdir s)
 
   (* State management *)
   | VernacWriteState s ->
-    unsupported_attributes atts;
-    vernac_write_state s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_write_state s)
   | VernacRestoreState s ->
-    unsupported_attributes atts;
-    vernac_restore_state s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_restore_state s)
 
   (* Commands *)
   | VernacCreateHintDb (dbname,b) ->
-    with_module_locality ~atts vernac_create_hintdb dbname b;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_create_hintdb dbname b)
   | VernacRemoveHints (dbnames,ids) ->
-    with_module_locality ~atts vernac_remove_hints dbnames ids;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_remove_hints dbnames ids)
   | VernacHints (dbnames,hints) ->
-    vernac_hints ~atts dbnames hints;
-    pstate
+    VtDefault(fun () ->
+        vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    with_module_locality ~atts vernac_syntactic_definition id c b;
-    pstate
-  | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) ->
-    with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_syntactic_definition id c b)
+  | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
+    VtDefault(fun () ->
+        with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
   | VernacReserve bl ->
-    unsupported_attributes atts;
-    vernac_reserve bl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_reserve bl)
   | VernacGeneralizable gen ->
-    with_locality ~atts vernac_generalizable gen;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_generalizable gen)
   | VernacSetOpacity qidl ->
-    with_locality ~atts vernac_set_opacity qidl;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl)
   | VernacSetStrategy l ->
-    with_locality ~atts vernac_set_strategy l;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_set_strategy l)
   | VernacSetOption (export, key,v) ->
-    vernac_set_option ~local:(only_locality atts) export key v;
-    pstate
+    VtDefault(fun () ->
+        vernac_set_option ~local:(only_locality atts) export key v)
   | VernacRemoveOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_remove_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_remove_option key v)
   | VernacAddOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_add_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_option key v)
   | VernacMemOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_mem_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_mem_option key v)
   | VernacPrintOption key ->
-    unsupported_attributes atts;
-    vernac_print_option key;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_print_option key)
   | VernacCheckMayEval (r,g,c) ->
-    Feedback.msg_notice @@
-      vernac_check_may_eval ~pstate ~atts r g c;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@
+        vernac_check_may_eval ~pstate ~atts r g c)
   | VernacDeclareReduction (s,r) ->
-    with_locality ~atts vernac_declare_reduction s r;
-    pstate
+    VtDefault(fun () ->
+        with_locality ~atts vernac_declare_reduction s r)
   | VernacGlobalCheck c ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_global_check c;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_global_check c)
   | VernacPrint p ->
-    Feedback.msg_notice @@ vernac_print ~pstate ~atts p;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@ vernac_print ~pstate ~atts p)
   | VernacSearch (s,g,r) ->
-    unsupported_attributes atts;
-    vernac_search ~pstate ~atts s g r;
-    pstate
+    VtReadProofOpt(
+        unsupported_attributes atts;
+        vernac_search ~atts s g r)
   | VernacLocate l -> unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_locate ~pstate l;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@ vernac_locate ~pstate l)
   | VernacRegister (qid, r) ->
-    unsupported_attributes atts;
-    vernac_register ~pstate qid r;
-    pstate
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_register qid r)
   | VernacPrimitive (id, prim, typopt) ->
-    unsupported_attributes atts;
-    ComAssumption.do_primitive id prim typopt;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        ComAssumption.do_primitive id prim typopt)
   | VernacComments l ->
-    unsupported_attributes atts;
-    Flags.if_verbose Feedback.msg_info (str "Comments ok\n");
-    pstate
-
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Flags.if_verbose Feedback.msg_info (str "Comments ok\n"))
   (* Proof management *)
   | VernacFocus n ->
-    unsupported_attributes atts;
-    Option.map (vernac_focus n) pstate
+    VtModifyProof(unsupported_attributes atts;vernac_focus n)
   | VernacUnfocus ->
-    unsupported_attributes atts;
-    Option.map (vernac_unfocus ()) pstate
+    VtModifyProof(unsupported_attributes atts;vernac_unfocus)
   | VernacUnfocused ->
-    unsupported_attributes atts;
-    Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate;
-    pstate
+    VtReadProof(fun ~pstate ->
+      unsupported_attributes atts;
+      Feedback.msg_notice @@ vernac_unfocused ~pstate)
   | VernacBullet b ->
-    unsupported_attributes atts;
-    Option.map (vernac_bullet b) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_bullet b)
   | VernacSubproof n ->
-    unsupported_attributes atts;
-    Option.map (vernac_subproof n) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_subproof n)
   | VernacEndSubproof ->
-    unsupported_attributes atts;
-    Option.map (vernac_end_subproof ()) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_end_subproof)
   | VernacShow s ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_show ~pstate s;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+      unsupported_attributes atts;
+      Feedback.msg_notice @@ vernac_show ~pstate s)
   | VernacCheckGuard ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@
-      with_pstate ~pstate (vernac_check_guard);
-    pstate
+    VtReadProof(fun ~pstate ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_check_guard ~pstate)
   | VernacProof (tac, using) ->
+    VtModifyProof(fun ~pstate ->
     unsupported_attributes atts;
     let using = Option.append using (Proof_using.get_default_proof_using ()) in
     let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
     let usings = if Option.is_empty using then "using:no" else "using:yes" in
     Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
-    let pstate =
-      vernac_require_open_proof ~pstate (fun ~pstate:ontop ->
-          Proof_global.modify_current_pstate (fun pstate ->
-          let pstate = Proof_global.get_current_pstate ontop in
-          let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
-          Option.cata (vernac_set_used_variables ~pstate) pstate using)
-            ontop)
-    in
-    Some pstate
+    let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
+    Option.cata (vernac_set_used_variables ~pstate) pstate using)
   | VernacProofMode mn ->
-    unsupported_attributes atts;
-    pstate
+    VtDefault(fun () -> unsupported_attributes atts)
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
-    vernac_interp_phase (Vernacextend.call ~atts opn args) ~pstate
+    Vernacextend.type_vernac ~atts opn args
+
+(* "locality" is the prefix "Local" attribute, while the "local" component
+ * is the outdated/deprecated "Local" attribute of some vernacular commands
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let rec interp_expr ?proof ~atts ~st c =
+  let pstate = st.Vernacstate.proof in
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+  match c with
+
+  (* 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")
+  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
+
+  (* Resetting *)
+  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
+  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
+  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
+  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
+
+  (* This one is possible to handle here *)
+  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
+
+  (* Loading a file requires access to the control interpreter so
+     [vernac_load] is mutually-recursive with [interp_expr] *)
+  | VernacLoad (verbosely,fname) ->
+    unsupported_attributes atts;
+    vernac_load ?proof ~verbosely ~st fname
+
+  (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
+  | VernacEndProof e ->
+    unsupported_attributes atts;
+    vernac_end_proof ?proof ?pstate e
+
+  | v ->
+    let fv = translate_vernac ~atts v in
+    interp_typed_vernac ~pstate fv
 
 (* XXX: This won't properly set the proof mode, as of today, it is
    controlled by the STM. Thus, we would need access information from
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 2d3443d30a..6f8a4e8a3c 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -53,15 +53,16 @@ type vernac_when =
   | VtLater
 type vernac_classification = vernac_type * vernac_when
 
-type vernac_interp_phase =
+type typed_vernac =
   | VtDefault of (unit -> unit)
+  | VtNoProof of (unit -> unit)
   | VtCloseProof of (pstate:Proof_global.t -> unit)
   | VtOpenProof of (unit -> Proof_global.t)
   | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
   | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
   | VtReadProof of (pstate:Proof_global.t -> unit)
 
-type vernac_command = atts:Attributes.vernac_flags -> vernac_interp_phase
+type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -91,7 +92,7 @@ let warn_deprecated_command =
 
 (* Interpretation of a vernac command *)
 
-let call opn converted_args ~atts =
+let type_vernac opn converted_args ~atts =
   let phase = ref "Looking up command" in
   try
     let depr, callback = vinterp_map opn in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index f06f31d45b..60e371a6d9 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -71,19 +71,20 @@ type vernac_classification = vernac_type * vernac_when
 
 (** Interpretation of extended vernac phrases. *)
 
-type vernac_interp_phase =
+type typed_vernac =
   | VtDefault of (unit -> unit)
+  | VtNoProof of (unit -> unit)
   | VtCloseProof of (pstate:Proof_global.t -> unit)
   | VtOpenProof of (unit -> Proof_global.t)
   | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
   | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
   | VtReadProof of (pstate:Proof_global.t -> unit)
 
-type vernac_command = atts:Attributes.vernac_flags -> vernac_interp_phase
+type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
-val call : Vernacexpr.extend_name -> plugin_args -> vernac_command
+val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command
 
 (** {5 VERNAC EXTEND} *)