[STM] explicit handling of parsing states

DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.

This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.

Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.

Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).

Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

25 files changed, 512 insertions, 488 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 716a942d5c..f91aa569d4 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -83,7 +83,10 @@ let set_doc doc = ide_doc := Some doc
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
   let pa = Pcoq.Parsable.make (Stream.of_string s) in
-  let loc_ast = Stm.parse_sentence ~doc sid pa in
+  match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
+  | None -> assert false (* s is not an empty string *)
+  | Some (loc, ast) ->
+  let loc_ast = CAst.make ~loc ast in
   let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
   set_doc doc;
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
@@ -121,10 +124,10 @@ let query (route, (s,id)) =
 
 let annotate phrase =
   let doc = get_doc () in
-  let {CAst.loc;v=ast} =
-    let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
-    Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
-  in
+  let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
+  match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
+  | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
+  | Some (_, ast) ->
   (* XXX: Width should be a parameter of annotate... *)
   Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 19ae97da77..759e60fbca 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -439,7 +439,6 @@ module Module =
     let module_expr = Entry.create "module_expr"
     let module_type = Entry.create "module_type"
   end
-
 let epsilon_value f e =
   let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
   let ext = [None, None, [r]] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 352857d4cd..3203a25b46 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -41,6 +41,16 @@ end
    - static rules explicitly defined in files g_*.ml4
    - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
      VERNAC EXTEND (see e.g. file extratactics.ml4)
+
+   Note that parsing a Coq document is in essence stateful: the parser
+   needs to recognize commands that start proofs and use a different
+   parsing entry point for them.
+
+   We thus provide two different interfaces: the "raw" parsing
+   interface, in the style of camlp5, which provides more flexibility,
+   and a more specialize "parse_vernac" one, which will indeed adjust
+   the state as needed.
+
 *)
 
 (** Dynamic extension of rules
@@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
+
+(** Parsing state handling *)
+val freeze : marshallable:bool -> frozen_t
+val unfreeze : frozen_t -> unit
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index df4b647642..0cdf8fb5d8 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin"
 
 {
 
-let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater)
 
 }
 
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 8f0440a2a4..c4f8843e51 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function
              (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
          with
          | Vernacextend.VtSideff ids, _ when hard ->
-             Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+             Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
          | x -> x }
     -> { do_generate_principle false (List.map snd recsl) }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d9b19c1ae6..4c24f51b1e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -58,15 +58,8 @@ let new_entry name =
 let toplevel_selector = new_entry "vernac:toplevel_selector"
 let tacdef_body = new_entry "tactic:tacdef_body"
 
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
-    proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let _ =
-  let mode = {
-    Proof_global.name = "Classic";
-    set = (fun () -> Pvernac.set_command_entry tactic_mode);
-    reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
-  } in
-  Proof_global.register_proof_mode mode
+(* Registers [tactic_mode] as a parser for proof editing *)
+let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 1ea6ff84d4..cdee012a82 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,7 @@ open Obligations
 let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
 let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
-let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 31fb1c9abf..db8d1b20d8 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
            add_morphism_infer atts m n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts [] m s n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts binders m s n;
        }
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4cc73f419e..9ee9e7ae2c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -22,51 +22,6 @@ open Names
 
 module NamedDecl = Context.Named.Declaration
 
-(*** Proof Modes ***)
-
-(* Type of proof modes :
-    - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it *)
-type proof_mode_name = string
-type proof_mode = {
-  name : proof_mode_name ;
-  set : unit -> unit ;
-  reset : unit -> unit
-}
-
-let proof_modes = Hashtbl.create 6
-let find_proof_mode n =
-  try Hashtbl.find proof_modes n
-  with Not_found ->
-    CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
-
-let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (CEphemeron.create m)
-
-(* initial mode: standard mode *)
-let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
-let _ = register_proof_mode standard
-
-(* Default proof mode, to be set at the beginning of proofs. *)
-let default_proof_mode = ref (find_proof_mode "No")
-
-let get_default_proof_mode_name () =
-  (CEphemeron.default !default_proof_mode standard).name
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
-  Goptions.(declare_string_option {
-    optdepr = false;
-    optname = "default proof mode" ;
-    optkey = proof_mode_opt_name ;
-    optread = begin fun () ->
-      (CEphemeron.default !default_proof_mode standard).name
-    end;
-    optwrite = begin fun n ->
-      default_proof_mode := find_proof_mode n
-    end
-  })
-
 (*** Proof Global Environment ***)
 
 (* Extra info on proofs. *)
@@ -95,7 +50,6 @@ type pstate = {
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
   proof : Proof.t;
-  mode : proof_mode CEphemeron.key;
   universe_decl: UState.universe_decl;
   strength : Decl_kinds.goal_kind;
 }
@@ -109,23 +63,8 @@ let apply_terminator f = f
    to be resumed when the current proof is closed or aborted. *)
 let pstates = ref ([] : pstate list)
 
-(* Current proof_mode, for bookkeeping *)
-let current_proof_mode = ref !default_proof_mode
-
-(* combinators for proof modes *)
-let update_proof_mode () =
-  match !pstates with
-  | { mode = m } :: _ ->
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
-      current_proof_mode := m;
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
-  | _ ->
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
-      current_proof_mode := find_proof_mode "No"
-
 (* combinators for the current_proof lists *)
-let push a l = l := a::!l;
-  update_proof_mode ()
+let push a l = l := a::!l
 
 exception NoSuchProof
 let () = CErrors.register_handler begin function
@@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} =
 
 let discard_current () =
   if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
-
 let discard_all () = pstates := []
 
-(* [set_proof_mode] sets the proof mode to be used after it's called. It is
-    typically called by the Proof Mode command. *)
-let set_proof_mode m id =
-  pstates := List.map
-      (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
-      !pstates;
-  update_proof_mode ()
-
-let set_proof_mode mn =
-  set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
-
-let activate_proof_mode mode =
-  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_current_proof_mode () =
-  CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator
     proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
-    mode = find_proof_mode "No";
-    universe_decl = pl;
-    strength = kind } in
+    strength = kind;
+    universe_decl = pl } in
   push initial_state pstates
 
 let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
@@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina
     proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
-    mode = find_proof_mode "No";
-    universe_decl = pl;
-    strength = kind } in
+    strength = kind;
+    universe_decl = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
@@ -478,7 +398,7 @@ end
 let freeze ~marshallable =
   if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
   else !pstates
-let unfreeze s = pstates := s; update_proof_mode ()
+let unfreeze s = pstates := s
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
 let copy_terminators ~src ~tgt =
   assert(List.length src = List.length tgt);
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e762f3b7dc..40920f51a3 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,7 +13,6 @@
      environment. *)
 
 type t
-
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t
 val copy_terminators : src:t -> tgt:t -> t
-
-
-(**********************************************************)
-(* Proof Mode API                                         *)
-(* The current Proof Mode API is deprecated and a new one *)
-(* will be (hopefully) defined in 8.8                     *)
-(**********************************************************)
-
-(** Type of proof modes :
-    - A name
-    - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it 
-
-*)
-type proof_mode_name = string
-type proof_mode = {
-  name : proof_mode_name ;
-  set : unit -> unit ;
-  reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
-    in [set_default_proof_mode].
-    One mode is already registered - the standard mode - named "No",
-    It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-(* Can't make this deprecated due to limitations of camlp5 *)
-(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
-
-val proof_mode_opt_name : string list
-
-val get_default_proof_mode_name : unit -> proof_mode_name
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
-    typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val activate_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val disactivate_current_proof_mode : unit -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
diff --git a/stm/stm.ml b/stm/stm.ml
index 8ed7f2c866..dfe5581ed5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -126,8 +126,6 @@ type aast = {
 }
 let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
   | VernacPrint _
@@ -146,13 +144,13 @@ let update_global_env () =
 
 module Vcs_ = Vcs.Make(Stateid.Self)
 type future_proof = Proof_global.closed_proof_output Future.computation
-type proof_mode = string
+
 type depth = int
 type branch_type =
   [ `Master
-  | `Proof of proof_mode * depth
+  | `Proof of depth
   | `Edit of
-      proof_mode * Stateid.t * Stateid.t  * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
+      Stateid.t * Stateid.t  * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
 (* TODO 8.7 : split commands and tactics, since this type is too messy now *)
 type cmd_t = {
   ctac : bool; (* is a tactic *)
@@ -203,10 +201,10 @@ let summary_pstate = Evarutil.meta_counter_summary_tag,
                      Obligations.program_tcc_summary_tag
 
 type cached_state =
-  | Empty
-  | Error of Exninfo.iexn
-  | Valid of Vernacstate.t
-
+  | EmptyState
+  | ParsingState of Vernacstate.Parser.state
+  | FullState of Vernacstate.t
+  | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn
 type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
 
@@ -214,10 +212,16 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
   mutable n_reached : int;      (* debug cache: how many times was computed *)
   mutable n_goals : int;        (* open goals: indentation *)
   mutable state : cached_state; (* state value *)
+  mutable proof_mode : Pvernac.proof_mode option;
   mutable vcs_backup : 'vcs option * backup option;
 }
-let default_info () =
-  { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+let default_info proof_mode =
+  {
+    n_reached = 0; n_goals = 0;
+    state = EmptyState;
+    proof_mode;
+    vcs_backup = (None,None);
+  }
 
 module DynBlockData : Dyn.S = Dyn.Make ()
 
@@ -256,15 +260,15 @@ end = struct (* {{{ *)
     List.fold_left max 0
       (CList.map_filter
         (function
-         | { Vcs_.kind = `Proof (_,n) } -> Some n
+         | { Vcs_.kind = `Proof n } -> Some n
          | { Vcs_.kind = `Edit _ } -> Some 1
          | _ -> None)
         (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
 
   let find_proof_at_depth vcs pl =
     try List.find (function
-          | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
-          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.")
+          | _, { Vcs_.kind = `Proof n } -> Int.equal n pl
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
           | _ -> false)
         (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
     with Not_found -> failwith "find_proof_at_depth"
@@ -326,7 +330,7 @@ module VCS : sig
 
   type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
-  val init : stm_doc_type -> id -> doc
+  val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc
   (* val get_type : unit -> stm_doc_type *)
   val set_ldir : Names.DirPath.t -> unit
   val get_ldir : unit -> Names.DirPath.t
@@ -339,7 +343,7 @@ module VCS : sig
   val branches : unit -> Branch.t list
   val get_branch : Branch.t -> branch_type branch_info
   val get_branch_pos : Branch.t -> id
-  val new_node : ?id:Stateid.t -> unit -> id
+  val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id
   val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
   val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
   val delete_branch : Branch.t -> unit
@@ -356,6 +360,10 @@ module VCS : sig
   val goals : id -> int -> unit
   val set_state : id -> cached_state -> unit
   val get_state : id -> cached_state
+  val set_parsing_state : id -> Vernacstate.Parser.state -> unit
+  val get_parsing_state : id -> Vernacstate.Parser.state option
+  val get_proof_mode : id -> Pvernac.proof_mode option
+  val set_proof_mode : id -> Pvernac.proof_mode option -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : block_start:id -> block_stop:id -> vcs
@@ -369,7 +377,8 @@ module VCS : sig
 
   val proof_nesting : unit -> int
   val checkout_shallowest_proof_branch : unit -> unit
-  val propagate_sideff : action:seff_t -> unit
+  val propagate_sideff : action:seff_t -> Stateid.t list
+  val propagate_qed : unit -> unit
 
   val gc : unit -> unit
 
@@ -411,11 +420,11 @@ end = struct (* {{{ *)
       | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
     let is_green id =
       match get_info vcs id with
-      | Some { state = Valid _ } -> true
+      | Some { state = FullState _ } -> true
       | _ -> false in
     let is_red id =
       match get_info vcs id with
-      | Some { state = Error _ } -> true
+      | Some { state = ErrorState _ } -> true
       | _ -> false in
     let head = current_branch vcs in
     let heads =
@@ -517,10 +526,11 @@ end = struct (* {{{ *)
   let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
   let ldir = ref Names.DirPath.empty
 
-  let init dt id =
+  let init dt id ps =
     doc_type := dt;
     vcs := empty id;
-    vcs := set_info !vcs id (default_info ());
+    let info = { (default_info None) with state = ParsingState ps } in
+    vcs := set_info !vcs id info;
     dummy_doc
 
   let set_ldir ld =
@@ -545,9 +555,9 @@ end = struct (* {{{ *)
   let branches () = branches !vcs
   let get_branch head = get_branch !vcs head
   let get_branch_pos head = (get_branch head).pos
-  let new_node ?(id=Stateid.fresh ()) () =
+  let new_node ?(id=Stateid.fresh ()) proof_mode () =
     assert(Vcs_.get_info !vcs id = None);
-    vcs := set_info !vcs id (default_info ());
+    vcs := set_info !vcs id (default_info proof_mode);
     id
   let merge id ~ours ?into branch =
     vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
@@ -569,9 +579,39 @@ end = struct (* {{{ *)
     | Some x -> x
     | None -> raise Vcs_aux.Expired
   let set_state id s =
-    (get_info id).state <- s;
-    if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
+    let info = get_info id in
+    info.state <- s;
+    let is_full_state_valid = match s with
+      | FullState _ -> true
+      | EmptyState | ErrorState _ | ParsingState _ -> false
+    in
+    if async_proofs_is_master !cur_opt && is_full_state_valid then
+      Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
+
   let get_state id = (get_info id).state
+
+  let get_parsing_state id =
+    stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_string id) ++ str " }}}");
+    match (get_info id).state with
+    | FullState s -> Some s.Vernacstate.parsing
+    | ParsingState s -> Some s
+    | ErrorState (s,_) -> s
+    | EmptyState -> None
+
+  let set_parsing_state id ps =
+    let info = get_info id in
+    let new_state =
+      match info.state with
+      | FullState s -> assert false
+      | ParsingState s -> assert false
+      | ErrorState _ -> assert false
+      | EmptyState -> ParsingState ps
+    in
+    info.state <- new_state
+
+  let get_proof_mode id = (get_info id).proof_mode
+  let set_proof_mode id pm = (get_info id).proof_mode <- pm
+
   let reached id =
     let info = get_info id in
     info.n_reached <- info.n_reached + 1
@@ -582,28 +622,33 @@ end = struct (* {{{ *)
 
   let checkout_shallowest_proof_branch () =
     if List.mem edit_branch (Vcs_.branches !vcs) then begin
-      checkout edit_branch;
-      match get_branch edit_branch with
-      | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
-      | _ -> assert false
+      checkout edit_branch
     end else
       let pl = proof_nesting () in
       try
-        let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
-          | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
-        checkout branch;
-        stm_prerr_endline (fun () -> "mode:" ^ mode);
-        Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+        let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in
+        checkout branch
       with Failure _ ->
-        checkout Branch.master;
-        Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
+        checkout Branch.master
 
   (* copies the transaction on every open branch *)
   let propagate_sideff ~action =
+    List.map (fun b ->
+      checkout b;
+      let proof_mode = get_proof_mode @@ get_branch_pos b in
+      let id = new_node proof_mode () in
+      merge id ~ours:(Sideff action) ~into:b Branch.master;
+      id)
+    (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+
+  let propagate_qed () =
     List.iter (fun b ->
       checkout b;
-      let id = new_node () in
-      merge id ~ours:(Sideff action) ~into:b Branch.master)
+      let proof_mode = get_proof_mode @@ get_branch_pos b in
+      let id = new_node proof_mode () in
+      let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in
+      merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master;
+      set_parsing_state id parsing)
     (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
 
   let visit id = Vcs_aux.visit !vcs id
@@ -625,10 +670,12 @@ end = struct (* {{{ *)
   let slice ~block_start ~block_stop =
     let l = nodes_in_slice ~block_start ~block_stop in
     let copy_info v id =
+      let info = get_info id in
       Vcs_.set_info v id
-        { (get_info id) with state = Empty; vcs_backup = None,None } in
+        { info with state = EmptyState;
+                    vcs_backup = None,None } in
     let make_shallow = function
-      | Valid st -> Valid (Vernacstate.make_shallow st)
+      | FullState st -> FullState (Vernacstate.make_shallow st)
       | x -> x
     in
     let copy_info_w_state v id =
@@ -651,12 +698,14 @@ end = struct (* {{{ *)
       let v = copy_info v id in
       v) l v in
     (* Stm should have reached the beginning of proof *)
-    assert (match (get_info block_start).state with Valid _ -> true | _ -> false);
+    assert (match get_state block_start
+            with FullState _ -> true | _  -> false);
     (* We put in the new dag the most recent state known to master *)
     let rec fill id =
-      match (get_info id).state with
-      | Empty | Error _ -> fill (Vcs_aux.visit v id).next
-      | Valid _ -> copy_info_w_state v id in
+      match get_state id with
+      | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next
+      | FullState _ -> copy_info_w_state v id
+    in
     let v = fill block_stop in
     (* We put in the new dag the first state (since Qed shall run on it,
      * see check_task_aux) *)
@@ -753,13 +802,12 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 let state_of_id ~doc id =
-  try match (VCS.get_info id).state with
-    | Valid s -> `Valid (Some s)
-    | Error (e,_) -> `Error e
-    | Empty -> `Valid None
+  try match VCS.get_state id with
+    | FullState s -> `Valid (Some s)
+    | ErrorState (_,(e,_)) -> `Error e
+    | EmptyState | ParsingState _ -> `Valid None
   with VCS.Expired -> `Expired
 
-
 (****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
 
@@ -782,6 +830,7 @@ module State : sig
   val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
 
   val install_cached : Stateid.t -> unit
+  (* val install_parsing_state : Stateid.t -> unit *)
   val is_cached : ?cache:bool -> Stateid.t -> bool
   val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool
 
@@ -804,10 +853,6 @@ module State : sig
   val register_root_state : unit -> unit
   val restore_root_state : unit -> unit
 
-  (* Only for internal use to catch problems in parse_sentence, should
-     be removed in the state handling refactoring.  *)
-  val cur_id : Stateid.t ref
-
   val purify : ('a -> 'b) -> 'a -> 'b
 
 end = struct (* {{{ *)
@@ -824,6 +869,8 @@ end = struct (* {{{ *)
     Vernacstate.unfreeze_interp_state st.vernac_state;
     cur_id := st.id
 
+  let invalidate_cur_state () = cur_id := Stateid.dummy
+
   type proof_part =
     Proof_global.t *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
@@ -842,49 +889,58 @@ end = struct (* {{{ *)
     Summary.project_from_summary st Util.(pi3 summary_pstate)
 
   let cache_state ~marshallable id =
-    VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable))
+    VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
 
-  let freeze_invalid id iexn = VCS.set_state id (Error iexn)
+  let freeze_invalid id iexn =
+    let ps = VCS.get_parsing_state id in
+    VCS.set_state id (ErrorState (ps,iexn))
 
   let is_cached ?(cache=false) id only_valid =
     if Stateid.equal id !cur_id then
       try match VCS.get_info id with
-        | { state = Empty } when cache -> cache_state ~marshallable:false id; true
+        | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:false id; true
         | _ -> true
       with VCS.Expired -> false
     else
-      try match VCS.get_info id with
-        | { state = Empty } -> false
-        | { state = Valid _ } -> true
-        | { state = Error _ } -> not only_valid
+      try match VCS.get_state id with
+        | EmptyState | ParsingState _ -> false
+        | FullState _ -> true
+        | ErrorState _ -> not only_valid
       with VCS.Expired -> false
 
   let is_cached_and_valid ?cache id = is_cached ?cache id true
   let is_cached ?cache id = is_cached ?cache id false
 
   let install_cached id =
-    match VCS.get_info id with
-    | { state = Valid s } ->
+    match VCS.get_state id with
+    | FullState s ->
        Vernacstate.unfreeze_interp_state s;
        cur_id := id
 
-    | { state = Error ie } ->
+    | ErrorState (_,ie) ->
        Exninfo.iraise ie
 
-    | _ ->
-        (* coqc has a 1 slot cache and only for valid states *)
-        if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then ()
-        else anomaly Pp.(str "installing a non cached state.")
+    | EmptyState | ParsingState _ ->
+      (* coqc has a 1 slot cache and only for valid states *)
+      if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then
+        anomaly Pp.(str "installing a non cached state.")
+
+  (*
+  let install_parsing_state id =
+    if not (Stateid.equal id !cur_id) then begin
+      Vernacstate.Parser.install @@ VCS.get_parsing_state id
+    end
+     *)
 
   let get_cached id =
-    try match VCS.get_info id with
-    | { state = Valid s } -> s
+    try match VCS.get_state id with
+    | FullState s -> s
     | _ -> anomaly Pp.(str "not a cached state.")
     with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
 
   let assign id what =
     let open Vernacstate in
-    if VCS.get_state id <> Empty then () else
+    if VCS.get_state id <> EmptyState then () else
     try match what with
     | `Full s ->
          let s =
@@ -896,7 +952,7 @@ end = struct (* {{{ *)
                 ~src:(get_cached prev).proof ~tgt:s.proof }
             else s
            with VCS.Expired -> s in
-         VCS.set_state id (Valid s)
+         VCS.set_state id (FullState s)
     | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
@@ -912,7 +968,7 @@ end = struct (* {{{ *)
                  st
                end
                 } in
-           VCS.set_state id (Valid s)
+           VCS.set_state id (FullState s)
     with VCS.Expired -> ()
 
   let exn_on id ~valid (e, info) =
@@ -958,7 +1014,7 @@ end = struct (* {{{ *)
     with e ->
       let (e, info) = CErrors.push e in
       let good_id = !cur_id in
-      cur_id := Stateid.dummy;
+      invalidate_cur_state ();
       VCS.reached id;
       let ie =
         match Stateid.get info, safe_id with
@@ -1130,7 +1186,7 @@ module Backtrack : sig
   val branches_of : Stateid.t -> backup
 
   (* Returns the state that the command should backtract to *)
-  val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when
+  val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t
   val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
 
 end = struct (* {{{ *)
@@ -1205,30 +1261,30 @@ end = struct (* {{{ *)
     try
       match Vernacprop.under_control v with
       | VernacResetInitial ->
-          Stateid.initial, VtNow
+          Stateid.initial
       | VernacResetName {CAst.v=name} ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let id = VCS.cur_tip () in
           (try
             let oid =
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            oid, VtNow
+            oid
           with Not_found ->
-            id, VtNow)
+            id)
       | VernacBack n ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let id = VCS.cur_tip () in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          oid, VtNow
+          oid
       | VernacUndo n ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let id = VCS.cur_tip () in
           let oid = fold_until back_tactic n id in
-          oid, VtLater
+          oid
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let id = VCS.cur_tip () in
           let vcs =
             match (VCS.get_info id).vcs_backup with
             | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
@@ -1241,15 +1297,15 @@ end = struct (* {{{ *)
             0 id in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          oid, VtLater
+          oid
       | VernacAbortAll ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let id = VCS.cur_tip () in
           let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
-          oid, VtLater
+          oid
       | VernacBackTo id ->
-          Stateid.of_int id, VtNow
+          Stateid.of_int id
       | _ -> anomaly Pp.(str "incorrect VtMeta classification")
     with
     | Not_found ->
@@ -2331,8 +2387,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                  (Proofview.Goal.goal gl) goals_to_admit then
              Proofview.give_up else Proofview.tclUNIT ()
               end in
-           match (VCS.get_info base_state).state with
-           | Valid { Vernacstate.proof } ->
+           match VCS.get_state base_state with
+           | FullState { Vernacstate.proof } ->
                Proof_global.unfreeze proof;
                Proof_global.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
@@ -2469,7 +2525,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 VCS.create_proof_task_box nodes ~qed:id ~block_start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
-                | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
+                | { VCS.kind = `Edit (_,_, okeep, _) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
                     if okeep <> keep then
                       msg_warning(strbrk("The command closing the proof changed. "
@@ -2655,7 +2711,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   (* We must reset the whole state before creating a document! *)
   State.restore_root_state ();
 
-  let doc = VCS.init doc_type Stateid.initial in
+  let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
 
   (* Set load path; important, this has to happen before we declare
      the library below as [Declaremods/Library] will infer the module
@@ -2723,16 +2779,8 @@ let observe ~doc id =
 
 let finish ~doc =
   let head = VCS.current_branch () in
-  let doc =observe ~doc (VCS.get_branch_pos head) in
-  VCS.print ();
-  (* EJGA: Setting here the proof state looks really wrong, and it
-     hides true bugs cf bug #5363. Also, what happens with observe? *)
-  (* Some commands may by side effect change the proof mode *)
-  (match VCS.get_branch head with
-  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
-  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
-  | _ -> ()
-  ); doc
+  let doc = observe ~doc (VCS.get_branch_pos head) in
+  VCS.print (); doc
 
 let wait ~doc =
   let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in
@@ -2809,12 +2857,14 @@ let merge_proof_branch ~valid ?id qast keep brname =
   match brinfo with
   | { VCS.kind = `Proof _ } ->
       VCS.checkout VCS.Branch.master;
-      let id = VCS.new_node ?id () in
+      let id = VCS.new_node ?id None () in
+      let parsing = Option.get @@ VCS.get_parsing_state (VCS.cur_tip ()) in
       VCS.merge id ~ours:(Qed (qed None)) brname;
+      VCS.set_parsing_state id parsing;
       VCS.delete_branch brname;
-      VCS.propagate_sideff ~action:CherryPickEnv;
+      VCS.propagate_qed ();
       `Ok
-  | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
+  | { VCS.kind = `Edit (qed_id, master_id, _,_) } ->
       let ofp =
         match VCS.visit qed_id with
         | { step = `Qed ({ fproof }, _) } -> fproof
@@ -2846,25 +2896,32 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_back_meta_command ~newtip ~head oid aast w =
-    let id = VCS.new_node ~id:newtip () in
-    let { mine; others } = Backtrack.branches_of oid in
+
+(* We process a meta command found in the document *)
+let process_back_meta_command ~newtip ~head oid aast =
     let valid = VCS.get_branch_pos head in
+    let old_parsing = Option.get @@ VCS.get_parsing_state oid in
+
+    (* Merge in and discard all the branches currently open that were not open in `oid` *)
+    let { mine; others } = Backtrack.branches_of oid in
     List.iter (fun branch ->
         if not (List.mem_assoc branch (mine::others)) then
           ignore(merge_proof_branch ~valid aast VtDrop branch))
       (VCS.branches ());
+
+    (* We add a node on top of every branch, to represent state aliasing *)
     VCS.checkout_shallowest_proof_branch ();
     let head = VCS.current_branch () in
     List.iter (fun b ->
-        if not(VCS.Branch.equal b head) then begin
-          VCS.checkout b;
-          VCS.commit (VCS.new_node ()) (Alias (oid,aast));
-        end)
+        VCS.checkout b;
+        let id = if (VCS.Branch.equal b head) then Some newtip else None in
+        let proof_mode = VCS.get_proof_mode @@ VCS.cur_tip () in
+        let id = VCS.new_node ?id proof_mode () in
+        VCS.commit id (Alias (oid,aast));
+        VCS.set_parsing_state id old_parsing)
       (VCS.branches ());
     VCS.checkout_shallowest_proof_branch ();
-    VCS.commit id (Alias (oid,aast));
-    Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+    Backtrack.record (); `Ok
 
 let get_allow_nested_proofs =
   Goptions.declare_bool_option_and_ref
@@ -2873,6 +2930,7 @@ let get_allow_nested_proofs =
     ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
     ~value:false
 
+(** [process_transaction] adds a node in the document *)
 let process_transaction ~doc ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
@@ -2880,18 +2938,21 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
+    let head_parsing =
+      Option.get @@ VCS.(get_parsing_state (get_branch_pos head)) in
+    let proof_mode = VCS.(get_proof_mode (get_branch_pos head)) in
     let rc = begin
       stm_prerr_endline (fun () ->
         "  classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
       match c with
       (* Meta *)
       | VtMeta, _ ->
-        let id, w = Backtrack.undo_vernac_classifier expr ~doc in
-        process_back_meta_command ~newtip ~head id x w
+        let id = Backtrack.undo_vernac_classifier expr ~doc in
+        process_back_meta_command ~newtip ~head id x
 
       (* Query *)
       | VtQuery, w ->
-          let id = VCS.new_node ~id:newtip () in
+          let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             if VCS.is_vio_doc () &&
                VCS.((get_branch head).kind = `Master) &&
@@ -2899,10 +2960,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+          VCS.set_parsing_state id head_parsing;
+          Backtrack.record (); assert (w == VtLater); `Ok
 
       (* Proof *)
-      | VtStartProof (mode, guarantee, names), w ->
+      | VtStartProof (guarantee, names), w ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
            "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
@@ -2912,39 +2974,22 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
            |> Exninfo.iraise
          else
 
-          let id = VCS.new_node ~id:newtip () in
+          let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in
+          let id = VCS.new_node ~id:newtip proof_mode () in
           let bname = VCS.mk_branch_name x in
           VCS.checkout VCS.Branch.master;
           if VCS.Branch.equal head VCS.Branch.master then begin
             VCS.commit id (Fork (x, bname, guarantee, names));
-            VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1))
+            VCS.branch bname (`Proof (VCS.proof_nesting () + 1))
           end else begin
-            VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
+            VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
-          Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
-      | VtProofMode _, VtLater ->
-          anomaly(str"VtProofMode must be executed VtNow.")
-      | VtProofMode mode, VtNow ->
-          let id = VCS.new_node ~id:newtip () in
-          VCS.commit id (mkTransCmd x [] false `MainQueue);
-          List.iter
-            (fun bn -> match VCS.get_branch bn with
-            | { VCS.root; kind = `Master; pos } -> ()
-            | { VCS.root; kind = `Proof(_,d); pos } ->
-                VCS.delete_branch bn;
-                VCS.branch ~root ~pos bn (`Proof(mode,d))
-            | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } ->
-                VCS.delete_branch bn;
-                VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob)))
-            (VCS.branches ());
-          VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record ();
-          ignore(finish ~doc:dummy_doc);
-          `Ok
+          VCS.set_parsing_state id head_parsing;
+          Backtrack.record (); assert (w == VtLater); `Ok
+
       | VtProofStep { parallel; proof_block_detection = cblock }, w ->
-          let id = VCS.new_node ~id:newtip () in
+          let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             match parallel with
             | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
@@ -2954,21 +2999,25 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
              If/when and UI will make something useful with this piece of info,
              detection should occur here.
           detect_proof_block id cblock; *)
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+          VCS.set_parsing_state id head_parsing;
+          Backtrack.record (); assert (w == VtLater); `Ok
+
       | VtQed keep, w ->
           let valid = VCS.get_branch_pos head in
-          let rc = merge_proof_branch ~valid ~id:newtip x keep head in
+          let rc =
+            merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
+          Backtrack.record (); assert (w == VtLater);
           rc
 
       (* Side effect in a (still open) proof is replayed on all branches*)
       | VtSideff l, w ->
-          let id = VCS.new_node ~id:newtip () in
-          begin match (VCS.get_branch head).VCS.kind with
-          | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue);
-          | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue);
-          | `Proof _ ->
+          let id = VCS.new_node ~id:newtip proof_mode () in
+          let new_ids =
+            match (VCS.get_branch head).VCS.kind with
+            | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); []
+            | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); []
+            | `Proof _ ->
               VCS.checkout VCS.Branch.master;
               VCS.commit id (mkTransCmd x l true `MainQueue);
               (* We can't replay a Definition since universes may be differently
@@ -2976,10 +3025,27 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               let action = match Vernacprop.under_control x.expr with
                 | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
                 | _ -> ReplayCommand x in
-              VCS.propagate_sideff ~action;
-          end;
+              VCS.propagate_sideff ~action
+          in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+          Backtrack.record ();
+          let parsing_state =
+            begin match w with
+              | VtNow ->
+                (* We need to execute to get the new parsing state *)
+                ignore(finish ~doc:dummy_doc);
+                let parsing = Vernacstate.Parser.cur_state () in
+                (* If execution has not been put in cache, we need to save the parsing state *)
+                if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing;
+                parsing
+              | VtLater -> VCS.set_parsing_state id head_parsing; head_parsing
+            end
+          in
+          (* We save the parsing state on non-master branches *)
+          List.iter (fun id ->
+              if (VCS.get_info id).state == EmptyState then
+              VCS.set_parsing_state id parsing_state) new_ids;
+          `Ok
 
       (* Unknown: we execute it, check for open goals and propagate sideeff *)
       | VtUnknown, VtNow ->
@@ -2991,7 +3057,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
             |> Exninfo.iraise
           else
-            let id = VCS.new_node ~id:newtip () in
+            let id = VCS.new_node ~id:newtip proof_mode () in
           let head_id = VCS.get_branch_pos head in
           let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
           let step () =
@@ -3009,9 +3075,8 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
                 | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
                 | _ -> Doesn'tGuaranteeOpacity in
               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"];
+              VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
+              VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
             end else begin
               begin match (VCS.get_branch head).VCS.kind with
               | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
@@ -3019,7 +3084,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               | `Proof _ ->
                   VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
                   (* We hope it can be replayed, but we can't really know *)
-                  VCS.propagate_sideff ~action:(ReplayCommand x);
+                  ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
               end;
               VCS.checkout_shallowest_proof_branch ();
             end in
@@ -3028,6 +3093,17 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
 
       | VtUnknown, VtLater ->
           anomaly(str"classifier: VtUnknown must imply VtNow.")
+
+      | VtProofMode pm, VtNow ->
+        let proof_mode = Pvernac.lookup_proof_mode pm in
+        let id = VCS.new_node ~id:newtip proof_mode () in
+        VCS.commit id (mkTransCmd x [] false `MainQueue);
+        VCS.set_parsing_state id head_parsing;
+        Backtrack.record (); `Ok
+
+      | VtProofMode _, VtLater ->
+          anomaly(str"classifier: VtProofMode must imply VtNow.")
+
     end in
     let pr_rc rc = match rc with
       | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
@@ -3051,45 +3127,10 @@ let get_ast ~doc id =
 
 let stop_worker n = Slaves.cancel_worker n
 
-(* We must parse on top of a state id, it should be something like:
-
-   - get parsing information for that state.
-   - feed the parsable / parser with the right parsing information.
-   - call the parser
-
-   Now, the invariant in ensured by the callers, but this is a bit
-   problematic.
-*)
-exception End_of_input
-
-let parse_sentence ~doc sid pa =
-  (* XXX: Should this restore the previous state?
-     Using reach here to try to really get to the
-     proper state makes the error resilience code fail *)
-  (* Reach.known_state ~cache:`Yes sid; *)
-  let cur_tip = VCS.cur_tip () in
-  let real_tip = !State.cur_id in
-  if not (Stateid.equal sid cur_tip) then
-    user_err ~hdr:"Stm.parse_sentence"
-      (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
-       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
-       str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
-  if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then
-    Feedback.msg_debug
-      (str "Warning, the real tip doesn't match the current tip." ++
-       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
-       str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
-       str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
-       str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
-  Flags.with_option Flags.we_are_parsing (fun () ->
-      try
-        match Pcoq.Entry.parse Pvernac.main_entry pa with
-        | None            -> raise End_of_input
-        | Some (loc, cmd) -> CAst.make ~loc cmd
-      with e when CErrors.noncritical e ->
-        let (e, info) = CErrors.push e in
-        Exninfo.iraise (e, info))
-    ()
+let parse_sentence ~doc sid ~entry pa =
+  let ps = Option.get @@ VCS.get_parsing_state sid in
+  let proof_mode = VCS.get_proof_mode sid in
+  Vernacstate.Parser.parse ps (entry proof_mode) pa
 
 (* You may need to know the len + indentation of previous command to compute
  * the indentation of the current one.
@@ -3153,20 +3194,20 @@ let query ~doc ~at ~route s =
   State.purify (fun s ->
     if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
     else Reach.known_state ~doc ~cache:true at;
-    try
-      while true do
-        let { CAst.loc; v=ast } = parse_sentence ~doc at s in
-        let indentation, strlen = compute_indentation ?loc at in
-        let st = State.get_cached at in
-        let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
-        ignore(stm_vernac_interp ~route at st aast)
-      done;
-    with
-    | End_of_input -> ()
-    | exn ->
-      let iexn = CErrors.push exn in
-      Exninfo.iraise iexn
-    )
+      let rec loop () =
+        match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
+        | None -> ()
+        | Some (loc, ast) ->
+           let indentation, strlen = compute_indentation ~loc at in
+           let st = State.get_cached at in
+           let aast = {
+             verbose = true; indentation; strlen;
+             loc = Some loc; expr = ast } in
+           ignore(stm_vernac_interp ~route at st aast);
+           loop ()
+      in
+      loop ()
+  )
   s
 
 let edit_at ~doc id =
@@ -3204,21 +3245,21 @@ let edit_at ~doc id =
       | { step = `Sideff (ReplayCommand _,id) } -> id
       | { step = `Sideff _ } -> tip
       | { next } -> master_for_br root next in
-  let reopen_branch start at_id mode qed_id tip old_branch =
+  let reopen_branch start at_id qed_id tip old_branch =
     let master_id, cancel_switch, keep =
       (* Hum, this should be the real start_id in the cluster and not next *)
       match VCS.visit qed_id with
       | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
       | _ -> anomaly (str "ProofTask not ending with Qed.") in
     VCS.branch ~root:master_id ~pos:id
-      VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
+      VCS.edit_branch (`Edit (qed_id, master_id, keep, old_branch));
     VCS.delete_boxes_of id;
     cancel_switch := true;
     Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `Focus { stop = qed_id; start = master_id; tip } in
   let no_edit = function
-   | `Edit (pm, _,_,_,_) -> `Proof(pm,1)
+   | `Edit (_,_,_,_) -> `Proof 1
    | x -> x in
   let backto id bn =
     List.iter VCS.delete_branch (VCS.branches ());
@@ -3244,17 +3285,17 @@ let edit_at ~doc id =
       let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
       let branch_info =
         match snd (VCS.get_info id).vcs_backup with
-        | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn)
-        | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn)
+        | Some{ mine = bn, { VCS.kind = `Proof _ }} -> Some bn
+        | Some{ mine = _, { VCS.kind = `Edit(_,_,_,bn) }} -> Some bn
         | _ -> None in
       match focused, VCS.proof_task_box_of id, branch_info with
       | _, Some _, None -> assert false
-      | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
+      | false, Some { qed = qed_id ; lemma = start }, Some bn ->
           let tip = VCS.cur_tip () in
           if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch
-          then reopen_branch start id mode qed_id tip bn
+          then reopen_branch start id qed_id tip bn
           else backto id (Some bn)
-      | true, Some { qed = qed_id }, Some(mode,bn) ->
+      | true, Some { qed = qed_id }, Some bn ->
           if on_cur_branch id then begin
             assert false
           end else if is_ancestor_of_cur_branch id then begin
@@ -3273,7 +3314,7 @@ let edit_at ~doc id =
           end else begin
             anomaly(str"Cannot leave an `Edit branch open.")
           end
-      | false, None, Some(_,bn) -> backto id (Some bn)
+      | false, None, Some bn -> backto id (Some bn)
       | false, None, None -> backto id None
     in
     VCS.print ();
diff --git a/stm/stm.mli b/stm/stm.mli
index b6071fa56b..821ab59a43 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -93,16 +93,17 @@ val init_core : unit -> unit
 (** [new_doc opt] Creates a new document with options [opt] *)
 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.Parsable.t ->
-  Vernacexpr.vernac_control CAst.t
+(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state
+    [sid] and non terminal [entry]. [entry] receives in input the current proof
+    mode. [sid] should be associated with a valid parsing state (which may not
+    be the case if an error was raised at parsing time). *)
+val parse_sentence :
+  doc:doc -> Stateid.t ->
+  entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
 
 (* Reminder: A parsable [pa] is constructed using
    [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
 
-exception End_of_input
-
 (* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
    the state [ontop].
    The [ontop] parameter just asserts that the GUI is on
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 09f531ce13..710ddb5571 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -15,8 +15,6 @@ open CAst
 open Vernacextend
 open Vernacexpr
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-
 let string_of_parallel = function
   | `Yes (solve,abs) ->
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -32,9 +30,9 @@ let string_of_vernac_type = function
   | VtProofStep { parallel; proof_block_detection } ->
       "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
-  | VtProofMode s -> "ProofMode " ^ s
   | VtQuery -> "Query"
   | VtMeta -> "Meta "
+  | VtProofMode _ -> "Proof Mode"
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -57,7 +55,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
 let options_affecting_stm_scheduling =
   [ Attributes.universe_polymorphism_option_name;
     stm_allow_nested_proofs_option_name;
-    Proof_global.proof_mode_opt_name;
+    Vernacentries.proof_mode_opt_name;
   ]
 
 let classify_vernac e =
@@ -97,15 +95,15 @@ let classify_vernac e =
     | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
-      VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
        let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater
+        VtStartProof(guarantee, idents_of_name i), VtLater
     | VernacStartTheoremProof (_,l) ->
         let ids = List.map (fun (({v=i}, _), _) -> i) l in
        let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+        VtStartProof (guarantee,ids), VtLater
     | VernacFixpoint (discharge,l) ->
        let guarantee =
          if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
@@ -115,7 +113,7 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+        then VtStartProof (guarantee,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
        let guarantee =
@@ -126,7 +124,7 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+        then VtStartProof (guarantee,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
@@ -184,8 +182,8 @@ let classify_vernac e =
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
-    | VernacContext _ (* TASSI: unsure *)
-    | VernacProofMode _ -> VtSideff [], VtNow
+    | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
+    | VernacProofMode pm -> VtProofMode pm, VtNow
     (* These are ambiguous *)
     | VernacInstance _ -> VtUnknown, VtNow
     (* Stm will install a new classifier to handle these *)
@@ -211,10 +209,10 @@ let classify_vernac e =
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier e with
         | ( VtQuery | VtProofStep _ | VtSideff _
-          | VtProofMode _ | VtMeta), _ as x -> x
+          | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
-            VtNow
-        | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater)
+            VtLater
+        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)
   in
   static_control_classifier e
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e58b9ccac7..cdbe444e5b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -243,7 +243,7 @@ let set_prompt prompt =
 let parse_to_dot =
   let rec dot st = match Stream.next st with
     | Tok.KEYWORD ("."|"...") -> ()
-    | Tok.EOI -> raise Stm.End_of_input
+    | Tok.EOI -> ()
     | _ -> dot st
   in
   Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
@@ -257,12 +257,12 @@ let rec discard_to_dot () =
     Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
     | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
-    | Stm.End_of_input -> raise Stm.End_of_input
     | e when CErrors.noncritical e -> ()
 
 let read_sentence ~state input =
   (* XXX: careful with ignoring the state Eugene!*)
-  try G_toplevel.parse_toplevel input
+  let open Vernac.State in
+  try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -366,7 +366,6 @@ let top_goal_print ~doc c oldp newp =
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
 
-(* Careful to keep this loop tail-rec *)
 let rec vernac_loop ~state =
   let open CAst in
   let open Vernac.State in
@@ -379,26 +378,30 @@ let rec vernac_loop ~state =
   try
     let input = top_buffer.tokens in
     match read_sentence ~state input with
-    | {v=VernacBacktrack(bid,_,_)} ->
+    | Some { v = VernacBacktrack(bid,_,_) } ->
       let bid = Stateid.of_int bid in
       let doc, res = Stm.edit_at ~doc:state.doc bid in
       assert (res = `NewTip);
       let state = { state with doc; sid = bid } in
       vernac_loop ~state
 
-    | {v=VernacQuit} ->
+    | Some { v = VernacQuit } ->
       exit 0
-    | {v=VernacDrop} ->
+
+    | Some { v = VernacDrop } ->
       if Mltop.is_ocaml_top()
       then (drop_last_doc := Some state; state)
       else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
-    | {v=VernacControl c; loc} ->
+
+    | Some { v = VernacControl c; loc } ->
       let nstate = Vernac.process_expr ~state (make ?loc c) in
       top_goal_print ~doc:state.doc c state.proof nstate.proof;
       vernac_loop ~state:nstate
+
+    | None ->
+      top_stderr (fnl ()); exit 0
+
   with
-  | Stm.End_of_input ->
-    top_stderr (fnl ()); exit 0
   (* Exception printing should be done by the feedback listener,
      however this is not yet ready so we rely on the exception for
      now. *)
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 5aba3d6b0b..7f1cca277e 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,7 +21,7 @@ type vernac_toplevel =
   | VernacControl of vernac_control
 
 module Toplevel_ : sig
-  val vernac_toplevel : vernac_toplevel CAst.t Entry.t
+  val vernac_toplevel : vernac_toplevel CAst.t option Entry.t
 end = struct
   let gec_vernac s = Entry.create ("toplevel:" ^ s)
   let vernac_toplevel = gec_vernac "vernac_toplevel"
@@ -34,14 +34,14 @@ open Toplevel_
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_toplevel;
   vernac_toplevel: FIRST
-    [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop }
-      | IDENT "Quit"; "." -> { CAst.make VernacQuit }
+    [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) }
+      | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) }
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
-        { CAst.make (VernacBacktrack (n,m,p)) }
-      | cmd = Pvernac.main_entry ->
+        { Some (CAst.make (VernacBacktrack (n,m,p))) }
+      | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
-              | None -> raise Stm.End_of_input
-              | Some (loc,c) -> CAst.make ~loc (VernacControl c) }
+              | None -> None
+              | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) }
       ]
     ]
   ;
@@ -49,6 +49,8 @@ END
 
 {
 
-let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
+let vernac_toplevel pm =
+  Pvernac.Unsafe.set_tactic_entry pm;
+  vernac_toplevel
 
 }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d8465aac27..45ca658857 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -68,10 +68,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
       if ntip <> `NewTip then
         anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
 
-      (* Due to bug #5363 we cannot use observe here as we should,
-         it otherwise reveals bugs *)
-      (* Stm.observe nsid; *)
-      let ndoc = if check then Stm.finish ~doc else doc in
+      (* Force the command  *)
+      let ndoc = if check then Stm.observe ~doc nsid else doc in
       let new_proof = Proof_global.give_me_the_proof_opt () in
       { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
@@ -92,51 +90,37 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let in_echo = if echo then Some (open_utf8_file_in file) else None in
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
-  let in_pa   = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
-  let rstate  = ref state in
-  (* For beautify, list of parsed sids *)
-  let rids    = ref [] in
+  let in_pa =
+    Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let open State in
-  try
-    (* we go out of the following infinite loop when a End_of_input is
-     * raised, which means that we raised the end of the file being loaded *)
-    while true do
-      let { CAst.loc; _ } as ast =
-          Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa
-        (* If an error in parsing occurs, we propagate the exception
-           so the caller of load_vernac will take care of it. However,
-           in the future it could be possible that we want to handle
-           all the errors as feedback events, thus in this case we
-           should relay the exception here for convenience. A
-           possibility is shown below, however we may want to refactor
-           this code:
-
-        try Stm.parse_sentence !rsid in_pa
-        with
-        | any when not is_end_of_input any ->
-          let (e, info) = CErrors.push any in
-          let loc = Loc.get_loc info in
-          let msg = CErrors.iprint (e, info) in
-          Feedback.msg_error ?loc msg;
-          iraise (e, info)
-       *)
-      in
-      (* Printing of vernacs *)
-      Option.iter (vernac_echo ?loc) in_echo;
-
-      checknav_simple ast;
-      let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in
-      rids := state.sid :: !rids;
-      rstate := state;
-    done;
-    input_cleanup ();
-    !rstate, !rids, Pcoq.Parsable.comment_state in_pa
+
+  (* ids = For beautify, list of parsed sids *)
+  let rec loop state ids =
+    match
+      Stm.parse_sentence
+        ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
+    with
+    | None ->
+        input_cleanup ();
+        state, ids, Pcoq.Parsable.comment_state in_pa
+    | Some (loc, ast) ->
+        let ast = CAst.make ~loc ast in
+
+        (* Printing of AST for -compile-verbose *)
+        Option.iter (vernac_echo ~loc) in_echo;
+
+        checknav_simple ast;
+
+        let state =
+          Flags.silently (interp_vernac ~check ~interactive ~state) ast in
+
+        loop state (state.sid :: ids)
+  in
+  try loop state []
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     input_cleanup ();
-    match e with
-    | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
-    | reraise -> iraise (e, info)
+    iraise (e, info)
 
 let process_expr ~state loc_ast =
   checknav_deep loc_ast;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8f155adb8a..0dfbba0e83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
   | None -> standard_proof_terminator ?hook compute_guard
   | Some terminator -> terminator ?hook compute_guard
   in
-  let sign = 
+  let sign =
     match sign with
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
 
 let uvernac = create_universe "vernac"
 
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+  let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+    Hashtbl.create 19 in
+  let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+  let find_proof_mode ename =
+    try Hashtbl.find proof_mode ename
+    with Not_found ->
+      CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+  let lookup_proof_mode name =
+    if Hashtbl.mem proof_mode name then Some name
+    else None
+  in
+  register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
 module Vernac_ =
   struct
     let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
       ] in
       Pcoq.grammar_extend main_entry None (None, [None, None, rule])
 
-    let command_entry_ref = ref noedit_mode
+    let select_tactic_entry spec =
+      match spec with
+      | None -> noedit_mode
+      | Some ename -> find_proof_mode ename
+
     let command_entry =
       Pcoq.Entry.of_parser "command_entry"
-        (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+        (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end
 
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+  let set_tactic_entry oname = command_entry_ref := oname
+end
 
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+  Unsafe.set_tactic_entry proof_mode;
+  Vernac_.main_entry
 
 let () =
   register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index b2f8f71462..fa251281dc 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -14,6 +14,8 @@ open Vernacexpr
 
 val uvernac : gram_universe
 
+type proof_mode
+
 module Vernac_ :
   sig
     val gallina : vernac_expr Entry.t
@@ -24,13 +26,31 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
+    val main_entry : (Loc.t * vernac_control) option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
 
+(* To be removed when the parser is made functional wrt the tactic
+ * non terminal *)
+module Unsafe : sig
+  (* To let third party grammar entries reuse Vernac_ and
+   * do something with the proof mode *)
+  val set_tactic_entry : proof_mode option -> unit
+end
+
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+
+(** Grammar entry for tactics: proof mode(s).
+  By default Coq's grammar has an empty entry (non-terminal) for
+  tactics.  A plugin can register its non-terminal by providing a name
+  and a grammar entry.
+
+  For example the Ltac plugin register the "Classic" grammar
+  entry for parsing its tactics.
+  *)
 
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Entry.t
-val set_command_entry : vernac_expr Entry.t -> unit
+val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode
+val lookup_proof_mode : string -> proof_mode option
+val proof_mode_to_string : proof_mode -> string
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 26859cd2cf..996fe320f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,6 +489,28 @@ let vernac_notation ~module_local =
 let vernac_custom_entry ~module_local s =
   Metasyntax.declare_custom_entry module_local s
 
+(* Default proof mode, to be set at the beginning of proofs for
+   programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+  default_proof_mode :=
+    match Pvernac.lookup_proof_mode name with
+    | Some pm -> pm
+    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+  Goptions.declare_string_option Goptions.{
+    optdepr = false;
+    optname = "default proof mode" ;
+    optkey = proof_mode_opt_name;
+    optread = get_default_proof_mode_opt;
+    optwrite = set_default_proof_mode_opt;
+  }
+
 (***********)
 (* Gallina *)
 
@@ -2115,13 +2137,9 @@ exception End_of_input
 let vernac_load interp fname =
   if Proof_global.there_are_pending_proofs () then
     CErrors.user_err Pp.(str "Load is not supported inside proofs.");
-  let interp x =
-    let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
-    Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
-    interp x in
-  let parse_sentence = Flags.with_option Flags.we_are_parsing
+  let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Entry.parse Pvernac.main_entry po with
+    match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2132,7 +2150,15 @@ let vernac_load interp fname =
     let in_chan = open_utf8_file_in longfname in
     Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   begin
-    try while true do interp (snd (parse_sentence input)) done
+    try while true do
+        let proof_mode =
+          if Proof_global.there_are_pending_proofs () then
+            Some (get_default_proof_mode ())
+          else
+            None
+        in
+        interp (snd (parse_sentence proof_mode input));
+      done
     with End_of_input -> ()
   end;
   (* If Load left a proof open, we fail too. *)
@@ -2312,8 +2338,7 @@ let interp ?proof ~atts ~st c =
     Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
     Option.iter vernac_set_end_tac tac;
     Option.iter vernac_set_used_variables using
-  | VernacProofMode mn -> unsupported_attributes atts;
-    Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+  | VernacProofMode mn -> unsupported_attributes atts; ()
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8d8d7cfcf0..4fbd3849b0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,6 +10,11 @@
 
 val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
 
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list
+
 (** Vernacular entries *)
 val vernac_require :
   Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 05687afd8b..f5cf3401d0 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -29,15 +29,15 @@ type vernac_type =
       parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
-  (* To be removed *)
-  | VtProofMode of string
   (* Queries are commands assumed to be "pure", that is to say, they
      don't modify the interpretation state. *)
   | VtQuery
+  (* Commands that change the current proof mode *)
+  | VtProofMode of string
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d43eb1ee8..118907c31b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -45,15 +45,15 @@ type vernac_type =
       parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
-  (* To be removed *)
-  | VtProofMode of string
   (* Queries are commands assumed to be "pure", that is to say, they
      don't modify the interpretation state. *)
   | VtQuery
+  (* Commands that change the current proof mode *)
+  | VtProofMode of string
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 61540024ef..c691dc8559 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,10 +8,30 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module Parser = struct
+
+  type state = Pcoq.frozen_t
+
+  let init () = Pcoq.freeze ~marshallable:false
+
+  let cur_state () = Pcoq.freeze ~marshallable:false
+
+  let parse ps entry pa =
+    Pcoq.unfreeze ps;
+    Flags.with_option Flags.we_are_parsing (fun () ->
+      try Pcoq.Entry.parse entry pa
+      with e when CErrors.noncritical e ->
+        let (e, info) = CErrors.push e in
+        Exninfo.iraise (e, info))
+    ()
+
+end
+
 type t = {
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.t;      (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
+  parsing: Parser.state;
+  system : States.state; (* summary + libstack *)
+  proof : Proof_global.t; (* proof state *)
+  shallow : bool; (* is the state trimmed down (libstack) *)
 }
 
 let s_cache = ref None
@@ -37,11 +57,13 @@ let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (States.freeze ~marshallable);
     proof  = update_cache s_proof (Proof_global.freeze ~marshallable);
     shallow = false;
+    parsing = Parser.cur_state ();
   }
 
-let unfreeze_interp_state { system; proof } =
+let unfreeze_interp_state { system; proof; parsing } =
   do_if_not_cached s_cache States.unfreeze system;
-  do_if_not_cached s_proof Proof_global.unfreeze proof
+  do_if_not_cached s_proof Proof_global.unfreeze proof;
+  Pcoq.unfreeze parsing
 
 let make_shallow st =
   let lib = States.lib_of_state st.system in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed20cb935a..581c23386a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,10 +8,21 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module Parser : sig
+  type state
+
+  val init : unit -> state
+  val cur_state : unit -> state
+
+  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
 type t = {
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.t;      (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
+  parsing: Parser.state;
+  system : States.state; (* summary + libstack *)
+  proof : Proof_global.t; (* proof state *)
+  shallow : bool; (* is the state trimmed down (libstack) *)
 }
 
 val freeze_interp_state : marshallable:bool -> t