Merge PR #9263: [STM] explicit handling of parsing states

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes

28 files changed, 527 insertions, 488 deletions

diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
new file mode 100644
index 0000000000..ebd1b524da
--- /dev/null
+++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
+
+    mtac2_CI_REF=proof-mode
+    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+    ltac2_CI_REF=proof-mode
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    equations_CI_REF=proof-mode
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
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/lib/stateid.ml b/lib/stateid.ml
index 5485c4bf19..8f45f3605d 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -27,6 +27,8 @@ let get exn = Exninfo.get exn state_id_info
 let equal = Int.equal
 let compare = Int.compare
 
+let print id = Pp.int id
+
 module Self = struct
  type t = int
  let compare = compare
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 5d4b71a354..f6ce7ddc40 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -20,6 +20,7 @@ val initial : t
 val dummy : t
 val fresh : unit -> t
 val to_string : t -> string
+val print : t -> Pp.t
 
 val of_int : int -> t
 val to_int : t -> int
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