Merge PR #10215: Refine typing of vernacular commands

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares

15 files changed, 882 insertions, 673 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea66234993..9cc8467c57 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -309,7 +309,7 @@ let id_of_class cl =
 	  mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-let instance_hook k info global imps ?hook cst =
+let instance_hook info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst imps;
   let info = intern_info info in
   let env = Global.env () in
@@ -317,7 +317,7 @@ let instance_hook k info global imps ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
   (* XXX: Duplication of the declare_constant path *)
   let kind = IsDefinition Instance in
   let sigma =
@@ -331,9 +331,9 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
   let kn = Declare.declare_constant id cdecl in
   Declare.definition_message id;
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
-  instance_hook k info global imps ?hook (ConstRef kn)
+  instance_hook info global imps ?hook (ConstRef kn)
 
-let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
@@ -344,136 +344,78 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
       (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook k pri global imps (ConstRef cst)
+  instance_hook pri global imps (ConstRef cst)
 
-let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
-  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-  if program_mode then
-    let hook _ _ vis gr =
-      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      Impargs.declare_manual_implicits false gr imps;
-      let pri = intern_info pri in
-      let env = Global.env () in
-      let sigma = Evd.from_env env in
-      declare_instance env sigma (Some pri) (not global) (ConstRef cst)
-    in
-    let obls, constr, typ =
-      match term with
-      | Some t ->
-        let termtype = EConstr.of_constr termtype in
-        let obls, _, constr, typ =
-          Obligations.eterm_obligations env id sigma 0 t termtype
-        in obls, Some constr, typ
-      | None -> [||], None, termtype
-    in
-    let hook = Lemmas.mk_hook hook in
-    let ctx = Evd.evar_universe_context sigma in
-    let _progress = Obligations.add_definition id ?term:constr
-              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
-    pstate
-  else
-    Some Flags.(silently (fun () ->
-        (* spiwack: it is hard to reorder the actions to do
-           the pretyping after the proof has opened. As a
-           consequence, we use the low-level primitives to code
-           the refinement manually.*)
-        let gls = List.rev (Evd.future_goals sigma) in
-        let sigma = Evd.reset_future_goals sigma in
-        let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype)
-          ~hook:(Lemmas.mk_hook
-             (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
-        (* spiwack: I don't know what to do with the status here. *)
-        let pstate =
-          if not (Option.is_empty term) then
-            let init_refine =
-              Tacticals.New.tclTHENLIST [
-                Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
-                Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
-                Tactics.New.reduce_after_refine;
-              ]
-            in
-            let pstate, _ = Pfedit.by init_refine pstate in
-            pstate
-          else
-            let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
-            pstate
-        in
-        match tac with
-        | Some tac ->
-          let pstate, _ = Pfedit.by tac pstate in
-          pstate
-        | None ->
-          pstate) ())
-
-let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
-  let props =
-    match props with
-    | Some (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
-      Some (Inl fs)
-    | Some (_, t) -> Some (Inr t)
-    | None ->
-      if program_mode then Some (Inl [])
-      else None
+let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
+  let hook _ _ vis gr =
+    let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+    Impargs.declare_manual_implicits false gr imps;
+    let pri = intern_info pri in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    declare_instance env sigma (Some pri) (not global) (ConstRef cst)
   in
-  let subst, sigma =
-    match props with
-    | None ->
-      (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
-    | Some (Inr term) ->
-      let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in
-      Some (Inr (c, subst)), sigma
-    | Some (Inl props) ->
-      let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
-      let props, rest =
-        List.fold_left
-          (fun (props, rest) decl ->
-             if is_local_assum decl then
-               try
-                 let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
-                   | Name id, {CAst.v=id'} -> Id.equal id id'
-                   | Anonymous, _ -> false
-                 in
-                 let (loc_mid, c) = List.find is_id rest in
-                 let rest' = List.filter (fun v -> not (is_id v)) rest
-                 in
-                 let {CAst.loc;v=mid} = get_id loc_mid in
-                 List.iter (fun (n, _, x) ->
-                     if Name.equal n (Name mid) then
-                       Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
-                 c :: props, rest'
-               with Not_found ->
-                 ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
-             else props, rest)
-          ([], props) k.cl_props
-      in
-      match rest with
-      | (n, _) :: _ ->
-        unbound_method env' sigma k.cl_impl (get_id n)
-      | _ ->
-        let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
-        let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
-        Some (Inl res), sigma
+  let obls, constr, typ =
+    match term with
+    | Some t ->
+      let termtype = EConstr.of_constr termtype in
+      let obls, _, constr, typ =
+        Obligations.eterm_obligations env id sigma 0 t termtype
+      in obls, Some constr, typ
+    | None -> [||], None, termtype
   in
-  let term, termtype =
-    match subst with
-    | None -> let termtype = it_mkProd_or_LetIn cty ctx in
-      None, termtype
-    | Some (Inl subst) ->
-      let subst = List.fold_left2
-          (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-          [] subst (k.cl_props @ snd k.cl_context)
+  let hook = Lemmas.mk_hook hook in
+  let ctx = Evd.evar_universe_context sigma in
+  ignore(Obligations.add_definition id ?term:constr
+           ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+
+
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+  (* spiwack: it is hard to reorder the actions to do
+     the pretyping after the proof has opened. As a
+     consequence, we use the low-level primitives to code
+     the refinement manually.*)
+  let gls = List.rev (Evd.future_goals sigma) in
+  let sigma = Evd.reset_future_goals sigma in
+  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+      ~hook:(Lemmas.mk_hook
+               (fun _ _ _ -> instance_hook pri global imps ?hook)) in
+  (* spiwack: I don't know what to do with the status here. *)
+  let pstate =
+    if not (Option.is_empty term) then
+      let init_refine =
+        Tacticals.New.tclTHENLIST [
+          Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
+          Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
+          Tactics.New.reduce_after_refine;
+        ]
       in
-      let (app, ty_constr) = instance_constructor (k,u) subst in
-      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-      let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-      Some term, termtype
-    | Some (Inr (def, subst)) ->
-      let termtype = it_mkProd_or_LetIn cty ctx in
-      let term = it_mkLambda_or_LetIn def ctx in
-      Some term, termtype
+      let pstate, _ = Pfedit.by init_refine pstate in
+      pstate
+    else
+      let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
+      pstate
   in
+  match tac with
+  | Some tac ->
+    let pstate, _ = Pfedit.by tac pstate in
+    pstate
+  | None ->
+    pstate
+
+let do_instance_subst_constructor_and_ty subst k u ctx =
+  let subst =
+    List.fold_left2 (fun subst' s decl ->
+      if is_local_assum decl then s :: subst' else subst')
+    [] subst (k.cl_props @ snd k.cl_context)
+  in
+  let (app, ty_constr) = instance_constructor (k,u) subst in
+  let termtype = it_mkProd_or_LetIn ty_constr ctx in
+  let term = it_mkLambda_or_LetIn (Option.get app) ctx in
+  term, termtype
+
+let do_instance_resolve_TC term termtype sigma env =
   let sigma = Evarutil.nf_evar_map sigma in
   let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
   (* Try resolving fields that are typeclasses automatically. *)
@@ -484,17 +426,110 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
   (* Check that the type is free of evars now. *)
   Pretyping.check_evars env (Evd.from_env env) sigma termtype;
   let termtype = to_constr sigma termtype in
-  let pstate =
-    if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
-      let term = to_constr sigma (Option.get term) in
-      (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
-       None)
-    else if program_mode || Option.is_empty props then
-      declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
-    else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
-  id, pstate
-
-let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass =
+  termtype, sigma
+
+let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
+  let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
+  let props, rest =
+    List.fold_left
+      (fun (props, rest) decl ->
+         if is_local_assum decl then
+           try
+             let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
+               | Name id, {CAst.v=id'} -> Id.equal id id'
+               | Anonymous, _ -> false
+             in
+             let (loc_mid, c) = List.find is_id rest in
+             let rest' = List.filter (fun v -> not (is_id v)) rest
+             in
+             let {CAst.loc;v=mid} = get_id loc_mid in
+             List.iter (fun (n, _, x) ->
+                 if Name.equal n (Name mid) then
+                   Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
+             c :: props, rest'
+           with Not_found ->
+             ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
+         else props, rest)
+      ([], props) k.cl_props
+  in
+  match rest with
+  | (n, _) :: _ ->
+    unbound_method env' sigma k.cl_impl (get_id n)
+  | _ ->
+    let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
+    let sigma, res =
+      type_ctx_instance ~program_mode
+        (push_rel_context ctx' env') sigma kcl_props props subst in
+    res, sigma
+
+let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id =
+  let term, termtype =
+    if List.is_empty k.cl_props then
+     let term, termtype =
+       do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+     Some term, termtype
+    else
+      None, it_mkProd_or_LetIn cty ctx in
+  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+  Flags.silently (fun () ->
+      declare_instance_open sigma ?hook ~tac ~global ~poly
+        id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
+    ()
+
+let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
+  let term, termtype, sigma =
+    match props with
+    | (true, { CAst.v = CRecord fs }) ->
+      if List.length fs > List.length k.cl_props then
+        mismatched_props env' (List.map snd fs) k.cl_props;
+      let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in
+      let term, termtype =
+        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+      term, termtype, sigma
+    | (_, term) ->
+      let sigma, def =
+        interp_casted_constr_evars ~program_mode:false env' sigma term cty in
+      let termtype = it_mkProd_or_LetIn cty ctx in
+      let term = it_mkLambda_or_LetIn def ctx in
+      term, termtype, sigma in
+  let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in
+  if Evd.has_undefined sigma then
+    CErrors.user_err Pp.(str "Unsolved obligations remaining.")
+  else
+    let term = to_constr sigma term in
+    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+
+let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
+  let term, termtype, sigma =
+    match opt_props with
+    | Some (true, { CAst.v = CRecord fs }) ->
+      if List.length fs > List.length k.cl_props then
+        mismatched_props env' (List.map snd fs) k.cl_props;
+      let subst, sigma =
+        do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
+     let term, termtype =
+       do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+     Some term, termtype, sigma
+    | Some (_, term) ->
+      let sigma, def =
+        interp_casted_constr_evars ~program_mode:true env' sigma term cty in
+      let termtype = it_mkProd_or_LetIn cty ctx in
+      let term = it_mkLambda_or_LetIn def ctx in
+      Some term, termtype, sigma
+    | None ->
+      let subst, sigma =
+        do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in
+      let term, termtype =
+        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+      Some term, termtype, sigma in
+  let termtype, sigma = do_instance_resolve_TC term termtype sigma env in
+  if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
+    let term = to_constr sigma (Option.get term) in
+    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+  else
+    declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype
+
+let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
@@ -522,14 +557,12 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass
   let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
-let new_instance ~pstate ?(global=false) ~program_mode
-    poly instid ctx cl props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
-  let env = Global.env() in
+let new_instance_common ~program_mode ~generalize env instid ctx cl =
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     interp_instance_context ~program_mode env ~generalize ctx pl cl
   in
+  (* The name generator should not be here *)
   let id =
     match instid with
     | Name id -> id
@@ -538,13 +571,41 @@ let new_instance ~pstate ?(global=false) ~program_mode
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
-    cty k u ctx ctx' pri decl imps subst id props
+  id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
+
+let new_instance_interactive ?(global=false)
+    poly instid ctx cl
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+  id, do_instance_interactive env sigma ?hook ~tac ~global ~poly
+    cty k u ctx ctx' pri decl imps subst id
+
+let new_instance_program ?(global=false)
+    poly instid ctx cl opt_props
+    ?(generalize=true) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode:true ~generalize env instid ctx cl in
+  do_instance_program env env' sigma ?hook ~global ~poly
+    cty k u ctx ctx' pri decl imps subst id opt_props;
+  id
+
+let new_instance ?(global=false)
+    poly instid ctx cl props
+    ?(generalize=true) ?hook pri =
+  let env = Global.env() in
+  let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+  do_instance env env' sigma ?hook ~global ~poly
+    cty k u ctx ctx' pri decl imps subst id props;
+  id
 
 let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    interp_instance_context ~program_mode env ctx pl cl
+    interp_instance_context ~program_mode ~generalize:false env ctx pl cl
   in
-  do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
+  do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 8d5f3e3a06..e61935c87a 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,34 +31,41 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
 val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
-val declare_instance_constant :
-  typeclass ->
-  Hints.hint_info_expr (** priority *) ->
-  bool (** globality *) ->
-  Impargs.manual_explicitation list (** implicits *) ->
-  ?hook:(GlobRef.t -> unit) ->
-  Id.t (** name *) ->
-  UState.universe_decl ->
-  bool (** polymorphic *) ->
-  Evd.evar_map (** Universes *) ->
-  Constr.t (** body *) ->
-  Constr.types (** type *) ->
-  unit
+val new_instance_interactive :
+  ?global:bool (** Not global by default. *)
+  -> Decl_kinds.polymorphic
+  -> name_decl
+  -> local_binder_expr list
+  -> constr_expr
+  -> ?generalize:bool
+  -> ?tac:unit Proofview.tactic
+  -> ?hook:(GlobRef.t -> unit)
+  -> Hints.hint_info_expr
+  -> Id.t * Proof_global.t
 
 val new_instance :
-  pstate:Proof_global.t option
-  -> ?global:bool (** Not global by default. *)
-  -> program_mode:bool
+  ?global:bool (** Not global by default. *)
+  -> Decl_kinds.polymorphic
+  -> name_decl
+  -> local_binder_expr list
+  -> constr_expr
+  -> (bool * constr_expr)
+  -> ?generalize:bool
+  -> ?hook:(GlobRef.t -> unit)
+  -> Hints.hint_info_expr
+  -> Id.t
+
+val new_instance_program :
+  ?global:bool (** Not global by default. *)
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
   -> (bool * constr_expr) option
   -> ?generalize:bool
-  -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
-  -> Id.t * Proof_global.t option (* May open a proof *)
+  -> Id.t
 
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a428c42e49..7a4e6d8698 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,80 +255,79 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-  let pstate =
-  if List.exists Option.is_empty fixdefs then
-    (* Some bodies to define by proof *)
-    let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-                fixnames fixtypes fiximps in
-    let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-        fixdefs) in
-    let evd = Evd.from_ctx ctx in
-    Some
-    (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None)
-  else begin
-    (* We shortcut the proof process *)
-    let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-    let env = Global.env() in
-    let indexes = search_guard env indexes fixdecls in
-    let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
-    let fixdecls =
-      List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    let evd = Evd.from_ctx ctx in
-    let evd = Evd.restrict_universe_context evd vars in
-    let ctx = Evd.check_univ_decl ~poly evd pl in
-    let pl = Evd.universe_binders evd in
-    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
-              fixnames fixdecls fixtypes fiximps);
-    (* Declare the recursive definitions *)
-    fixpoint_message (Some indexes) fixnames;
-    None
-  end in
-  (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+let declare_fixpoint_notations ntns =
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+
+let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+  (* Some bodies to define by proof *)
+  let thms =
+    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
+              fixnames fixtypes fiximps in
+  let init_tac =
+    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
+      fixdefs) in
+  let evd = Evd.from_ctx ctx in
+  let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
+    evd pl (Some(false,indexes,init_tac)) thms None in
+  declare_fixpoint_notations ntns;
   pstate
 
-let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let pstate =
-  if List.exists Option.is_empty fixdefs then
-    (* Some bodies to define by proof *)
-    let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-                fixnames fixtypes fiximps in
-    let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-        fixdefs) in
-    let evd = Evd.from_ctx ctx in
-    Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
-            evd pl (Some(true,[],init_tac)) thms None)
-  else begin
-    (* We shortcut the proof process *)
-    let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-    let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Vars.universes_of_constr (List.hd fixdecls) in
-    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    let evd = Evd.from_ctx ctx in
-    let evd = Evd.restrict_universe_context evd vars in
-    let ctx = Evd.check_univ_decl ~poly evd pl in
-    let pl = Evd.universe_binders evd in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
-              fixnames fixdecls fixtypes fiximps);
-    (* Declare the recursive definitions *)
-    cofixpoint_message fixnames;
-    None
-  end in
-  (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+  (* We shortcut the proof process *)
+  let fixdefs = List.map Option.get fixdefs in
+  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let env = Global.env() in
+  let indexes = search_guard env indexes fixdecls in
+  let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+  let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+  let fixdecls =
+    List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+  let evd = Evd.from_ctx ctx in
+  let evd = Evd.restrict_universe_context evd vars in
+  let ctx = Evd.check_univ_decl ~poly evd pl in
+  let pl = Evd.universe_binders evd in
+  let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
+            fixnames fixdecls fixtypes fiximps);
+  (* Declare the recursive definitions *)
+  fixpoint_message (Some indexes) fixnames;
+  declare_fixpoint_notations ntns
+
+let declare_cofixpoint_notations = declare_fixpoint_notations
+
+let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  (* Some bodies to define by proof *)
+  let thms =
+    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
+              fixnames fixtypes fiximps in
+  let init_tac =
+    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
+      fixdefs) in
+  let evd = Evd.from_ctx ctx in
+  let pstate = Lemmas.start_proof_with_initialization
+    (Global,poly, DefinitionBody CoFixpoint)
+    evd pl (Some(true,[],init_tac)) thms None in
+  declare_cofixpoint_notations ntns;
   pstate
 
+let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  (* We shortcut the proof process *)
+  let fixdefs = List.map Option.get fixdefs in
+  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+  let vars = Vars.universes_of_constr (List.hd fixdecls) in
+  let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
+  let evd = Evd.from_ctx ctx in
+  let evd = Evd.restrict_universe_context evd vars in
+  let ctx = Evd.check_univ_decl ~poly evd pl in
+  let pl = Evd.universe_binders evd in
+  ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+            fixnames fixdecls fixtypes fiximps);
+  (* Declare the recursive definitions *)
+  cofixpoint_message fixnames;
+  declare_cofixpoint_notations ntns
+
 let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
   | CStructRec na -> na
   | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
@@ -366,18 +365,33 @@ let check_safe () =
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint ~ontop local poly l =
+let do_fixpoint_common l =
   let fixl, ntns = extract_fixpoint_components ~structonly:true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
-  let possible_indexes =
-    List.map compute_possible_guardness_evidences info in
-  let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+  fixl, ntns, fix, List.map compute_possible_guardness_evidences info
+
+let do_fixpoint_interactive local poly l =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
+  let pstate = declare_fixpoint_interactive local poly fix possible_indexes ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
 
-let do_cofixpoint ~ontop local poly l =
+let do_fixpoint local poly l =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
+  declare_fixpoint local poly fix possible_indexes ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+
+let do_cofixpoint_common l =
   let fixl,ntns = extract_cofixpoint_components l in
-  let cofix = interp_fixpoint ~cofix:true fixl ntns in
-  let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
+  ntns, interp_fixpoint ~cofix:true fixl ntns
+
+let do_cofixpoint_interactive local poly l =
+  let ntns, cofix = do_cofixpoint_common l in
+  let pstate = declare_cofixpoint_interactive local poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   pstate
+
+let do_cofixpoint local poly l =
+  let ntns, cofix = do_cofixpoint_common l in
+  declare_cofixpoint local poly cofix ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 5937842f17..c8d617da5f 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -18,15 +18,17 @@ open Vernacexpr
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
+val do_fixpoint_interactive :
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t
+
 val do_fixpoint :
-  ontop:Proof_global.t option ->
-  (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+
+val do_cofixpoint_interactive :
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t
 
 val do_cofixpoint :
-  ontop:Proof_global.t option ->
-  (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
@@ -83,20 +85,16 @@ val interp_fixpoint :
 
 (** [Not used so far] *)
 val declare_fixpoint :
-  ontop:Proof_global.t option ->
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Proof_global.lemma_possible_guards -> decl_notation list ->
-  Proof_global.t option
+  Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  ontop:Proof_global.t option ->
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  decl_notation list ->
-  Proof_global.t option
+  decl_notation list -> unit
 
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5eec8aed1e..63e6dd247f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -50,7 +50,6 @@ let def_body = Entry.create "vernac:def_body"
 let decl_notation = Entry.create "vernac:decl_notation"
 let record_field = Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
-let instance_name = Entry.create "vernac:instance_name"
 let section_subset_expr = Entry.create "vernac:section_subset_expr"
 
 let make_bullet s =
@@ -683,7 +682,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina_ext instance_name hint_info;
+  GLOBAL: gallina_ext hint_info;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 740b9031cc..d14c7ddf8f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -207,12 +207,8 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
-let fresh_name_for_anonymous_theorem ~pstate =
-  let avoid = match pstate with
-  | None -> Id.Set.empty
-  | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate)
-  in
-  next_global_ident_away default_thm_id avoid
+let fresh_name_for_anonymous_theorem () =
+  next_global_ident_away default_thm_id Id.Set.empty
 
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
@@ -329,7 +325,7 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
   let terminator = match terminator with
   | None -> standard_proof_terminator ?hook compute_guard
   | Some terminator -> terminator ?hook compute_guard
@@ -340,7 +336,7 @@ let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?
     | None -> initialize_named_context_for_proof ()
   in
   let goals = [ Global.env_of_context sign , c ] in
-  Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator
+  Proof_global.start_proof sigma id ?pl kind goals terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -356,7 +352,7 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms snl =
+let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
   let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
@@ -388,14 +384,14 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
-      let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let pstate = Proof_global.simple_with_current_proof (fun _ p ->
+      let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+      let pstate = Proof_global.modify_proof (fun p ->
           match init_tac with
           | None -> p
           | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
       pstate
 
-let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
+let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -427,7 +423,7 @@ let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_proof_with_initialization ~ontop ?hook kind evd decl recguard thms snl
+  start_proof_with_initialization ?hook kind evd decl recguard thms snl
 
 (* Saving a proof *)
 
@@ -487,20 +483,26 @@ let save_proof_admitted ?proof ~pstate =
   in
   Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
 
-let save_proof_proved ?proof ?pstate ~opaque ~idopt =
+let save_pstate_proved ~pstate ~opaque ~idopt =
+  let obj, terminator = Proof_global.close_proof ~opaque
+      ~keep_body_ucst_separate:false (fun x -> x) pstate
+  in
+  Proof_global.(apply_terminator terminator (Proved (opaque, idopt, obj)))
+
+let save_proof_proved ?proof ?ontop ~opaque ~idopt =
   (* Invariant (uh) *)
-  if Option.is_empty pstate && Option.is_empty proof then
+  if Option.is_empty ontop && Option.is_empty proof then
     user_err (str "No focused proof (No proof-editing in progress).");
   let (proof_obj,terminator) =
     match proof with
     | None ->
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
-      let pstate = Option.get pstate in
+      let pstate = Proof_global.get_current_pstate @@ Option.get ontop in
       Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
     | Some proof -> proof
   in
   (* if the proof is given explicitly, nothing has to be deleted *)
-  let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in
+  let ontop = if Option.is_empty proof then Proof_global.discard_current Option.(get ontop) else ontop in
   Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
-  pstate
+  ontop
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1f70cfa1ad..3df543156d 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -37,7 +37,7 @@ val call_hook
   -> ?fix_exn:Future.fix_exn
   -> hook_type
 
-val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val ->
   ?compute_guard:Proof_global.lemma_possible_guards ->
@@ -45,12 +45,11 @@ val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_dec
 
 val start_proof_com
   :  program_mode:bool
-  -> ontop:Proof_global.t option
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
   -> Proof_global.t
 
-val start_proof_with_initialization : ontop:Proof_global.t option ->
+val start_proof_with_initialization :
   ?hook:declaration_hook ->
   goal_kind -> Evd.evar_map -> UState.universe_decl ->
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
@@ -62,7 +61,7 @@ val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
   Proof_global.proof_terminator
 
-val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t
+val fresh_name_for_anonymous_theorem : unit -> Id.t
 
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
@@ -78,7 +77,13 @@ val save_proof_admitted
 
 val save_proof_proved
   :  ?proof:Proof_global.closed_proof
-  -> ?pstate:Proof_global.t
+  -> ?ontop:Proof_global.stack
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
-  -> Proof_global.t option
+  -> Proof_global.stack option
+
+val save_pstate_proved
+  : pstate:Proof_global.t
+  -> opaque:Proof_global.opacity_flag
+  -> idopt:Names.lident option
+  -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bc741a0ec7..0d93e19723 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -760,7 +760,7 @@ let update_obls prg obls rem =
       match prg'.prg_deps with
       | [] ->
           let kn = declare_definition prg' in
-	    progmap_remove prg';
+            progmap_remove prg';
 	    Defined kn
       | l ->
 	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
@@ -944,7 +944,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
       ignore (auto (Some prg.prg_name) None deps)
   end
 
-let rec solve_obligation ~ontop prg num tac =
+let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -965,19 +965,19 @@ let rec solve_obligation ~ontop prg num tac =
     Proof_global.make_terminator
       (obligation_terminator prg.prg_name num guard ?hook auto) in
   let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
-  let pstate = Lemmas.start_proof ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
+  let pstate = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
   let pstate = fst @@ Pfedit.by !default_tactic pstate in
   let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
   pstate
 
-and obligation ~ontop (user_num, name, typ) tac =
+and obligation (user_num, name, typ) tac =
   let num = pred user_num in
   let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num >= 0 && num < Array.length obls then
       let obl = obls.(num) in
 	match obl.obl_body with
-          | None -> solve_obligation ~ontop prg num tac
+          | None -> solve_obligation prg num tac
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
 
@@ -1177,7 +1177,7 @@ let admit_obligations n =
     let prg = get_prog_err n in
     admit_prog prg
 
-let next_obligation ~ontop n tac =
+let next_obligation n tac =
   let prg = match n with
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
@@ -1188,7 +1188,7 @@ let next_obligation ~ontop n tac =
   | Some i -> i
   | None -> anomaly (Pp.str "Could not find a solvable obligation.")
   in
-  solve_obligation ~ontop prg i tac
+  solve_obligation prg i tac
 
 let check_program_libraries () =
   Coqlib.check_required_library Coqlib.datatypes_module_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 9214ddd4b9..3b77039de5 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -86,14 +86,12 @@ val add_mutual_definitions :
   fixpoint_kind -> unit
 
 val obligation
-  :  ontop:Proof_global.t option
-  -> int * Names.Id.t option * Constrexpr.constr_expr option
+  : int * Names.Id.t option * Constrexpr.constr_expr option
   -> Genarg.glob_generic_argument option
   -> Proof_global.t
 
 val next_obligation
-  :  ontop:Proof_global.t option
-  -> Names.Id.t option
+  : Names.Id.t option
   -> Genarg.glob_generic_argument option
   -> Proof_global.t
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 337cb233a2..18e0fde296 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -47,15 +47,20 @@ let vernac_pperr_endline pp =
 let there_are_pending_proofs ~pstate =
   not Option.(is_empty pstate)
 
-let check_no_pending_proof ~pstate =
-  if there_are_pending_proofs ~pstate then
-    user_err Pp.(str "Command not supported (Open proofs remain)")
-
+(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *)
 let vernac_require_open_proof ~pstate f =
   match pstate with
   | Some pstate -> f ~pstate
   | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
 
+let with_pstate ~pstate f =
+  vernac_require_open_proof ~pstate
+    (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
+
+ let modify_pstate ~pstate f =
+   vernac_require_open_proof ~pstate (fun ~pstate ->
+       Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
+
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -91,6 +96,25 @@ module DefAttributes = struct
     { polymorphic; program; locality; deprecated }
 end
 
+let with_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  f ~local
+
+let with_section_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let section_local = make_section_locality local in
+  f ~section_local
+
+let with_module_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let module_local = make_module_locality local in
+  f ~module_local
+
+let with_def_attributes ~atts f =
+  let atts = DefAttributes.parse atts in
+  if atts.DefAttributes.program then Obligations.check_program_libraries ();
+  f ~atts
+
 (*******************)
 (* "Show" commands *)
 
@@ -540,7 +564,7 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ~program_mode ~pstate ?hook k l =
+let start_proof_and_print ~program_mode ?hook k l =
   let inference_hook =
     if program_mode then
       let hook env sigma ev =
@@ -562,7 +586,7 @@ let start_proof_and_print ~program_mode ~pstate ?hook k l =
       in Some hook
     else None
   in
-  start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l
+  start_proof_com ~program_mode ?inference_hook ?hook k l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -573,60 +597,63 @@ let vernac_definition_hook p = function
   Some (Class.add_subclass_hook p)
 | _ -> None
 
-let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
+let vernac_definition_name lid local =
+  let lid =
+    match lid with
+    | { v = Name.Anonymous; loc } ->
+         CAst.make ?loc (fresh_name_for_anonymous_theorem ())
+    | { v = Name.Name n; loc } -> CAst.make ?loc n in
+  let () =
+    match local with
+    | Discharge -> Dumpglob.dump_definition lid true "var"
+    | Local | Global -> Dumpglob.dump_definition lid false "def"
+  in
+  lid
+
+let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
-  let () =
-    match id with
-    | Anonymous -> ()
-    | Name n -> let lid = CAst.make ?loc n in
-      match local with
-      | Discharge -> Dumpglob.dump_definition lid true "var"
-      | Local | Global -> Dumpglob.dump_definition lid false "def"
-  in
   let program_mode = atts.program in
-  let name =
-    match id with
-    | Anonymous -> fresh_name_for_anonymous_theorem ~pstate
-    | Name n -> n
-  in
-  (match def with
-    | ProveBody (bl,t) ->   (* local binders, typ *)
-      Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind)
-              ?hook [(CAst.make ?loc name, pl), (bl, t)])
-    | DefineBody (bl,red_option,c,typ_opt) ->
-      let red_option = match red_option with
-        | None -> None
-        | Some r ->
-          let sigma, env = get_current_or_global_context ~pstate in
-          Some (snd (Hook.get f_interp_redexp env sigma r)) in
-      ComDefinition.do_definition ~program_mode name
-        (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
-      pstate
-  )
+  let name = vernac_definition_name lid local in
+  start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
 
-let vernac_start_proof ~atts ~pstate kind l =
+let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
+  let open DefAttributes in
+  let local = enforce_locality_exp atts.locality discharge in
+  let hook = vernac_definition_hook atts.polymorphic kind in
+  let program_mode = atts.program in
+  let name = vernac_definition_name lid local in
+  let red_option = match red_option with
+    | None -> None
+    | Some r ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      Some (snd (Hook.get f_interp_redexp env sigma r)) in
+  ComDefinition.do_definition ~program_mode name.v
+    (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook
+
+(* NB: pstate argument to use combinators easily *)
+let vernac_start_proof ~atts kind l =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
+  start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
 
-let vernac_end_proof ?pstate ?proof = function
+let vernac_end_proof ?pstate:ontop ?proof = function
   | Admitted ->
-    vernac_require_open_proof ~pstate (save_proof_admitted ?proof);
-    pstate
+    with_pstate ~pstate:ontop (save_proof_admitted ?proof);
+    ontop
   | Proved (opaque,idopt) ->
-    save_proof_proved ?pstate ?proof ~opaque ~idopt
+    save_proof_proved ?ontop ?proof ~opaque ~idopt
 
 let vernac_exact_proof ~pstate c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
-  let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
-  if not status then Feedback.feedback Feedback.AddedAxiom;
-  pstate
+  let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
@@ -804,30 +831,46 @@ let vernac_inductive ~atts cum lo finite indl =
       in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
     *)
 
-let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
-  let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
+let vernac_fixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  (* XXX: Switch to the attribute system and match on ~atts *)
-  let do_fixpoint = if atts.program then
-      fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
-    else
-      ComFixpoint.do_fixpoint ~ontop:pstate
-  in
-  do_fixpoint local atts.polymorphic l
+  enforce_locality_exp atts.DefAttributes.locality discharge
 
-let vernac_cofixpoint ~atts ~pstate discharge l =
+let vernac_fixpoint_interactive ~atts discharge l =
   let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
+  let local = vernac_fixpoint_common ~atts discharge l in
+  if atts.program then
+    CErrors.user_err Pp.(str"Program Fixpoint requires a body");
+  ComFixpoint.do_fixpoint_interactive local atts.polymorphic l
+
+let vernac_fixpoint ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_fixpoint_common ~atts discharge l in
+  if atts.program then
+    (* XXX: Switch to the attribute system and match on ~atts *)
+    ComProgramFixpoint.do_fixpoint local atts.polymorphic l
+  else
+    ComFixpoint.do_fixpoint local atts.polymorphic l
+
+let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  let do_cofixpoint = if atts.program then
-      fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
-    else
-      ComFixpoint.do_cofixpoint ~ontop:pstate
-  in
-  do_cofixpoint local atts.polymorphic l
+  enforce_locality_exp atts.DefAttributes.locality discharge
+
+let vernac_cofixpoint_interactive ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_cofixpoint_common ~atts discharge l in
+  if atts.program then
+    CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
+  ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l
+
+let vernac_cofixpoint ~atts discharge l =
+  let open DefAttributes in
+  let local = vernac_cofixpoint_common ~atts discharge l in
+  if atts.program then
+    ComProgramFixpoint.do_cofixpoint local atts.polymorphic l
+  else
+    ComFixpoint.do_cofixpoint local atts.polymorphic l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -883,14 +926,13 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
 
-let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
+let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
-       check_no_pending_proof ~pstate;
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -930,13 +972,12 @@ let vernac_end_module export {loc;v=id} =
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
 
-let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
 
   match mty_ast_l with
     | [] ->
-       check_no_pending_proof ~pstate;
        let binders_ast,argsexport =
 	 List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -983,8 +1024,7 @@ let vernac_include l =
 
 (* Sections *)
 
-let vernac_begin_section ~pstate ({v=id} as lid) =
-  check_no_pending_proof ~pstate;
+let vernac_begin_section ({v=id} as lid) =
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
@@ -997,8 +1037,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
 
 (* Dispatcher of the "End" command *)
 
-let vernac_end_segment ~pstate ({v=id} as lid) =
-  check_no_pending_proof ~pstate;
+let vernac_end_segment ({v=id} as lid) =
   match Lib.find_opening_node id with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1058,18 +1097,42 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~atts name bl t props pri =
-  let open DefAttributes in
-  let global = not (make_section_locality atts.locality) in
+let vernac_instance_program ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let program_mode = atts.program in
-  Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
+  ()
+
+let vernac_instance_interactive ~atts name bl t info =
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  let _id, pstate =
+    Classes.new_instance_interactive ~global polymorphic name bl t info in
+  pstate
+
+let vernac_instance ~atts name bl t props info =
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  let _id : Id.t =
+    Classes.new_instance ~global polymorphic name bl t props info in
+  ()
 
 let vernac_declare_instance ~atts id bl inst pri =
-  let open DefAttributes in
-  let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_definition (fst id) false "inst";
-  Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri
 
 let vernac_context ~poly l =
   if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
@@ -1094,7 +1157,7 @@ let focus_command_cond = Proof.no_cond command_focus
      all tactics fail if there are no further goals to prove. *)
 
 let vernac_solve_existential ~pstate n com =
-  Proof_global.simple_with_current_proof (fun _ p ->
+  Proof_global.modify_proof (fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -1118,9 +1181,7 @@ let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
         (str "Unknown variable: " ++ Id.print id))
     l;
   let _, pstate = Proof_global.set_used_variables pstate l in
-  fst @@ Proof_global.with_current_proof begin fun _ p ->
-    (p, ())
-  end pstate
+  pstate
 
 (*****************************)
 (* Auxiliary file management *)
@@ -1928,7 +1989,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let sigma, env = get_current_or_global_context ~pstate in
     print_about env sigma ref_or_by_not udecl
 
-let vernac_print ~(pstate : Proof_global.t option) ~atts =
+let vernac_print ~pstate ~atts =
   let sigma, env = get_current_or_global_context ~pstate in
   function
   | PrintTables -> print_tables ()
@@ -2085,10 +2146,8 @@ let vernac_locate ~pstate = function
   | LocateOther (s, qid) -> print_located_other s qid
   | LocateFile f -> locate_file f
 
-let vernac_register ~pstate qid r =
+let vernac_register qid r =
   let gr = Smartlocate.global_with_alias qid in
-  if there_are_pending_proofs ~pstate then
-    user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   match r with
   | RegisterInline ->
     begin match gr with
@@ -2116,19 +2175,21 @@ let vernac_register ~pstate qid r =
 (********************)
 (* Proof management *)
 
-let vernac_focus gln =
-  Proof_global.simple_with_current_proof (fun _ p ->
+let vernac_focus ~pstate gln =
+  Proof_global.modify_proof (fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
          user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.")
       | Some n ->
          Proof.focus focus_command_cond () n p)
+    pstate
 
   (* Unfocuses one step in the focus stack. *)
-let vernac_unfocus () =
-  Proof_global.simple_with_current_proof
-    (fun _ p -> Proof.unfocus command_focus p ())
+let vernac_unfocus ~pstate =
+  Proof_global.modify_proof
+    (fun p -> Proof.unfocus command_focus p ())
+    pstate
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
@@ -2145,29 +2206,33 @@ let vernac_unfocused ~pstate =
 let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
-let vernac_subproof gln =
-  Proof_global.simple_with_current_proof (fun _ p ->
+let vernac_subproof gln ~pstate =
+  Proof_global.modify_proof (fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
     | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
     | _ -> user_err ~hdr:"bracket_selector"
              (str "Brackets do not support multi-goal selectors."))
+    pstate
 
-let vernac_end_subproof () =
-  Proof_global.simple_with_current_proof (fun _ p ->
-    Proof.unfocus subproof_kind p ())
+let vernac_end_subproof ~pstate =
+  Proof_global.modify_proof (fun p ->
+      Proof.unfocus subproof_kind p ())
+    pstate
 
-let vernac_bullet (bullet : Proof_bullet.t) =
-  Proof_global.simple_with_current_proof (fun _ p ->
-    Proof_bullet.put p bullet)
+let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
+  Proof_global.modify_proof (fun p ->
+    Proof_bullet.put p bullet) pstate
 
+(* Stack is needed due to show proof names, should deprecate / remove
+   and take pstate *)
 let vernac_show ~pstate =
   match pstate with
   (* Show functions that don't require a proof state *)
   | None ->
     begin function
-      | ShowProof -> show_proof ~pstate
+      | ShowProof -> show_proof ~pstate:None
       | ShowMatch id -> show_match id
       | _ ->
         user_err (str "This command requires an open proof.")
@@ -2185,7 +2250,7 @@ let vernac_show ~pstate =
     | ShowExistentials -> show_top_evars ~pstate
     | ShowUniverses -> show_universes ~pstate
     | ShowProofNames ->
-      pr_sequence Id.print (Proof_global.get_all_proof_names pstate)
+      Id.print (Proof_global.get_current_proof_name pstate)
     | ShowIntros all -> show_intro ~pstate all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
@@ -2203,26 +2268,6 @@ let vernac_check_guard ~pstate =
       (str ("Condition violated: ") ++s)
   in message
 
-(* Attributes *)
-let with_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  f ~local
-
-let with_section_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let section_local = make_section_locality local in
-  f ~section_local
-
-let with_module_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let module_local = make_module_locality local in
-  f ~module_local
-
-let with_def_attributes ~atts f =
-  let atts = DefAttributes.parse atts in
-  if atts.DefAttributes.program then Obligations.check_program_libraries ();
-  f ~atts
-
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
@@ -2277,338 +2322,388 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
-(* "locality" is the prefix "Local" attribute, while the "local" component
- * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility.
- * loc is the Loc.t of the vernacular command being interpreted. *)
-let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
-  let pstate = st.Vernacstate.proof in
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+let interp_typed_vernac c ~pstate =
+  let open Proof_global in
+  let open Vernacextend in
   match c with
-
-  (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
-  | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
-  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
-
-  (* Resetting *)
-  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
-  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
-  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
-  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
-
-  (* This one is possible to handle here *)
-  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
-
-  (* Loading a file requires access to the control interpreter so
-     [vernac_load] is mutually-recursive with [interp_expr] *)
-  | VernacLoad (verbosely,fname) ->
-    unsupported_attributes atts;
-    vernac_load ?proof ~verbosely ~st fname
-
+  | VtDefault f -> f (); pstate
+  | VtNoProof f ->
+    if there_are_pending_proofs ~pstate then
+      user_err Pp.(str "Command not supported (Open proofs remain)");
+    let () = f () in
+    pstate
+  | VtCloseProof f ->
+    vernac_require_open_proof ~pstate (fun ~pstate ->
+        f ~pstate:(Proof_global.get_current_pstate pstate);
+        Proof_global.discard_current pstate)
+  | VtOpenProof f ->
+    Some (push ~ontop:pstate (f ()))
+  | VtModifyProof f ->
+    modify_pstate f ~pstate
+  | VtReadProofOpt f ->
+    f ~pstate:(Option.map get_current_pstate pstate);
+    pstate
+  | VtReadProof f ->
+    with_pstate ~pstate f;
+    pstate
+
+(* We interpret vernacular commands to a DSL that specifies their
+   allowed actions on proof states *)
+let translate_vernac ~atts v = let open Vernacextend in match v with
+  | VernacEndProof _
+  | VernacAbortAll
+  | VernacRestart
+  | VernacUndo _
+  | VernacUndoTo _
+  | VernacResetName _
+  | VernacResetInitial
+  | VernacBack _
+  | VernacBackTo _
+  | VernacAbort _
+  | VernacLoad _ ->
+    anomaly (str "type_vernac")
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-    with_module_locality ~atts vernac_syntax_extension infix sl;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl)
   | VernacDeclareScope sc ->
-    with_module_locality ~atts vernac_declare_scope sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_declare_scope sc)
   | VernacDelimiters (sc,lr) ->
-    with_module_locality ~atts vernac_delimiters sc lr;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_delimiters sc lr)
   | VernacBindScope (sc,rl) ->
-    with_module_locality ~atts vernac_bind_scope sc rl;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_bind_scope sc rl)
   | VernacOpenCloseScope (b, s) ->
-    with_section_locality ~atts vernac_open_close_scope (b,s);
-    pstate
+    VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
   | VernacInfix (mv,qid,sc) ->
-    with_module_locality ~atts vernac_infix mv qid sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
   | VernacNotation (c,infpl,sc) ->
-    with_module_locality ~atts vernac_notation c infpl sc;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
   | VernacNotationAddFormat(n,k,v) ->
-    unsupported_attributes atts;
-    Metasyntax.add_notation_extra_printing_rule n k v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Metasyntax.add_notation_extra_printing_rule n k v)
   | VernacDeclareCustomEntry s ->
-    with_module_locality ~atts vernac_custom_entry s;
-    pstate
+    VtDefault(fun () -> with_module_locality ~atts vernac_custom_entry s)
 
   (* Gallina *)
-  | VernacDefinition ((discharge,kind),lid,d) ->
-    with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d
+
+  | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) ->
+    VtDefault (fun () ->
+      with_def_attributes ~atts
+       vernac_definition discharge lid bl red_option c typ)
+  | VernacDefinition (discharge,lid,ProveBody(bl,typ)) ->
+    VtOpenProof(fun () ->
+      with_def_attributes ~atts
+       vernac_definition_interactive discharge lid bl typ)
+
   | VernacStartTheoremProof (k,l) ->
-    with_def_attributes ~atts vernac_start_proof ~pstate k l
-  | VernacEndProof e ->
-    unsupported_attributes atts;
-    vernac_end_proof ?proof ?pstate e
+    VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l)
   | VernacExactProof c ->
-    unsupported_attributes atts;
-    vernac_require_open_proof ~pstate (vernac_exact_proof c)
+    VtCloseProof(fun ~pstate ->
+        unsupported_attributes atts;
+        vernac_exact_proof ~pstate c)
+
+  | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
+    let i () =
+      unsupported_attributes atts;
+      vernac_define_module export lid bl mtys mexprl in
+    (* XXX: We should investigate if eventually this should be made
+       VtNoProof in all cases. *)
+    if List.is_empty mexprl then VtNoProof i else VtDefault i
+
+  | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_declare_module_type lid bl mtys mtyo)
   | VernacAssumption ((discharge,kind),nl,l) ->
-    with_def_attributes ~atts vernac_assumption discharge kind l nl;
-    pstate
+    VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl)
   | VernacInductive (cum, priv, finite, l) ->
-    vernac_inductive ~atts cum priv finite l;
-    pstate
+    VtDefault(fun () -> vernac_inductive ~atts cum priv finite l)
   | VernacFixpoint (discharge, l) ->
-    with_def_attributes ~atts vernac_fixpoint ~pstate discharge l
+    let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in
+    if opens then
+      VtOpenProof (fun () ->
+        with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
+    else
+      VtDefault (fun () ->
+        with_def_attributes ~atts vernac_fixpoint discharge l)
   | VernacCoFixpoint (discharge, l) ->
-    with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l
+    let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in
+    if opens then
+      VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
+    else
+      VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l)
+
   | VernacScheme l ->
-    unsupported_attributes atts;
-    vernac_scheme l;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_scheme l)
   | VernacCombinedScheme (id, l) ->
-    unsupported_attributes atts;
-    vernac_combined_scheme id l;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_combined_scheme id l)
   | VernacUniverse l ->
-    vernac_universe ~poly:(only_polymorphism atts) l;
-    pstate
+    VtDefault(fun () -> vernac_universe ~poly:(only_polymorphism atts) l)
   | VernacConstraint l ->
-    vernac_constraint ~poly:(only_polymorphism atts) l;
-    pstate
+    VtDefault(fun () -> vernac_constraint ~poly:(only_polymorphism atts) l)
 
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
-    unsupported_attributes atts;
-    vernac_declare_module export lid bl mtyo;
-    pstate
-  | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
-    unsupported_attributes atts;
-    vernac_define_module ~pstate export lid bl mtys mexprl;
-    pstate
-  | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
-    unsupported_attributes atts;
-    vernac_declare_module_type ~pstate lid bl mtys mtyo;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_declare_module export lid bl mtyo)
   | VernacInclude in_asts ->
-    unsupported_attributes atts;
-    vernac_include in_asts;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_include in_asts)
   (* Gallina extensions *)
   | VernacBeginSection lid ->
-    unsupported_attributes atts;
-    vernac_begin_section ~pstate lid;
-    pstate
-
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_begin_section lid)
   | VernacEndSegment lid ->
-    unsupported_attributes atts;
-    vernac_end_segment ~pstate lid;
-    pstate
-
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_end_segment lid)
   | VernacNameSectionHypSet (lid, set) ->
-    unsupported_attributes atts;
-    vernac_name_sec_hyp lid set;
-    pstate
-
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_name_sec_hyp lid set)
   | VernacRequire (from, export, qidl) ->
-    unsupported_attributes atts;
-    vernac_require from export qidl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_require from export qidl)
   | VernacImport (export,qidl) ->
-    unsupported_attributes atts;
-    vernac_import export qidl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_import export qidl)
   | VernacCanonical qid ->
-    unsupported_attributes atts;
-    vernac_canonical qid;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_canonical qid)
   | VernacCoercion (r,s,t) ->
-    vernac_coercion ~atts r s t;
-    pstate
+    VtDefault(fun () -> vernac_coercion ~atts r s t)
   | VernacIdentityCoercion ({v=id},s,t) ->
-    vernac_identity_coercion ~atts id s t;
-    pstate
+    VtDefault(fun () -> vernac_identity_coercion ~atts id s t)
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info)
+    let { DefAttributes.program } = DefAttributes.parse atts in
+    if program then
+      VtDefault (fun () -> vernac_instance_program ~atts name bl t props info)
+    else begin match props with
+    | None ->
+       VtOpenProof(fun () ->
+        vernac_instance_interactive ~atts name bl t info)
+    | Some props ->
+       VtDefault(fun () ->
+        vernac_instance ~atts name bl t props info)
+    end
+
   | VernacDeclareInstance (id, bl, inst, info) ->
-    with_def_attributes ~atts vernac_declare_instance id bl inst info;
-    pstate
+    VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info)
   | VernacContext sup ->
-    let () = vernac_context ~poly:(only_polymorphism atts) sup in
-    pstate
+    VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup)
   | VernacExistingInstance insts ->
-    with_section_locality ~atts vernac_existing_instance insts;
-    pstate
+    VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts)
   | VernacExistingClass id ->
-    unsupported_attributes atts;
-    vernac_existing_class id;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_existing_class id)
 
   (* Solving *)
   | VernacSolveExistential (n,c) ->
-    unsupported_attributes atts;
-    Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c))
-
+    VtModifyProof(fun ~pstate ->
+        unsupported_attributes atts;
+        vernac_solve_existential ~pstate n c)
   (* Auxiliary file and library management *)
   | VernacAddLoadPath (isrec,s,alias) ->
-    unsupported_attributes atts;
-    vernac_add_loadpath isrec s alias;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_loadpath isrec s alias)
   | VernacRemoveLoadPath s ->
-    unsupported_attributes atts;
-    vernac_remove_loadpath s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_remove_loadpath s)
   | VernacAddMLPath (isrec,s) ->
-    unsupported_attributes atts;
-    vernac_add_ml_path isrec s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_ml_path isrec s)
   | VernacDeclareMLModule l ->
-    with_locality ~atts vernac_declare_ml_module l;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
   | VernacChdir s ->
-    unsupported_attributes atts;
-    vernac_chdir s;
-    pstate
+    VtDefault(fun () -> unsupported_attributes atts; vernac_chdir s)
 
   (* State management *)
   | VernacWriteState s ->
-    unsupported_attributes atts;
-    vernac_write_state s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_write_state s)
   | VernacRestoreState s ->
-    unsupported_attributes atts;
-    vernac_restore_state s;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_restore_state s)
 
   (* Commands *)
   | VernacCreateHintDb (dbname,b) ->
-    with_module_locality ~atts vernac_create_hintdb dbname b;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_create_hintdb dbname b)
   | VernacRemoveHints (dbnames,ids) ->
-    with_module_locality ~atts vernac_remove_hints dbnames ids;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_remove_hints dbnames ids)
   | VernacHints (dbnames,hints) ->
-    vernac_hints ~atts dbnames hints;
-    pstate
+    VtDefault(fun () ->
+        vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    with_module_locality ~atts vernac_syntactic_definition id c b;
-    pstate
-  | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) ->
-    with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags;
-    pstate
+    VtDefault(fun () ->
+        with_module_locality ~atts vernac_syntactic_definition id c b)
+  | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
+    VtDefault(fun () ->
+        with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
   | VernacReserve bl ->
-    unsupported_attributes atts;
-    vernac_reserve bl;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_reserve bl)
   | VernacGeneralizable gen ->
-    with_locality ~atts vernac_generalizable gen;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_generalizable gen)
   | VernacSetOpacity qidl ->
-    with_locality ~atts vernac_set_opacity qidl;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl)
   | VernacSetStrategy l ->
-    with_locality ~atts vernac_set_strategy l;
-    pstate
+    VtDefault(fun () -> with_locality ~atts vernac_set_strategy l)
   | VernacSetOption (export, key,v) ->
-    vernac_set_option ~local:(only_locality atts) export key v;
-    pstate
+    VtDefault(fun () ->
+        vernac_set_option ~local:(only_locality atts) export key v)
   | VernacRemoveOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_remove_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_remove_option key v)
   | VernacAddOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_add_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_add_option key v)
   | VernacMemOption (key,v) ->
-    unsupported_attributes atts;
-    vernac_mem_option key v;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_mem_option key v)
   | VernacPrintOption key ->
-    unsupported_attributes atts;
-    vernac_print_option key;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        vernac_print_option key)
   | VernacCheckMayEval (r,g,c) ->
-    Feedback.msg_notice @@
-      vernac_check_may_eval ~pstate ~atts r g c;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@
+        vernac_check_may_eval ~pstate ~atts r g c)
   | VernacDeclareReduction (s,r) ->
-    with_locality ~atts vernac_declare_reduction s r;
-    pstate
+    VtDefault(fun () ->
+        with_locality ~atts vernac_declare_reduction s r)
   | VernacGlobalCheck c ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_global_check c;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_global_check c)
   | VernacPrint p ->
-    Feedback.msg_notice @@ vernac_print ~pstate ~atts p;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@ vernac_print ~pstate ~atts p)
   | VernacSearch (s,g,r) ->
-    unsupported_attributes atts;
-    vernac_search ~pstate ~atts s g r;
-    pstate
+    VtReadProofOpt(
+        unsupported_attributes atts;
+        vernac_search ~atts s g r)
   | VernacLocate l -> unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_locate ~pstate l;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+        Feedback.msg_notice @@ vernac_locate ~pstate l)
   | VernacRegister (qid, r) ->
-    unsupported_attributes atts;
-    vernac_register ~pstate qid r;
-    pstate
+    VtNoProof(fun () ->
+        unsupported_attributes atts;
+        vernac_register qid r)
   | VernacPrimitive (id, prim, typopt) ->
-    unsupported_attributes atts;
-    ComAssumption.do_primitive id prim typopt;
-    pstate
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        ComAssumption.do_primitive id prim typopt)
   | VernacComments l ->
-    unsupported_attributes atts;
-    Flags.if_verbose Feedback.msg_info (str "Comments ok\n");
-    pstate
-
+    VtDefault(fun () ->
+        unsupported_attributes atts;
+        Flags.if_verbose Feedback.msg_info (str "Comments ok\n"))
   (* Proof management *)
   | VernacFocus n ->
-    unsupported_attributes atts;
-    Option.map (vernac_focus n) pstate
+    VtModifyProof(unsupported_attributes atts;vernac_focus n)
   | VernacUnfocus ->
-    unsupported_attributes atts;
-    Option.map (vernac_unfocus ()) pstate
+    VtModifyProof(unsupported_attributes atts;vernac_unfocus)
   | VernacUnfocused ->
-    unsupported_attributes atts;
-    Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate;
-    pstate
+    VtReadProof(fun ~pstate ->
+      unsupported_attributes atts;
+      Feedback.msg_notice @@ vernac_unfocused ~pstate)
   | VernacBullet b ->
-    unsupported_attributes atts;
-    Option.map (vernac_bullet b) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_bullet b)
   | VernacSubproof n ->
-    unsupported_attributes atts;
-    Option.map (vernac_subproof n) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_subproof n)
   | VernacEndSubproof ->
-    unsupported_attributes atts;
-    Option.map (vernac_end_subproof ()) pstate
+    VtModifyProof(
+      unsupported_attributes atts;
+      vernac_end_subproof)
   | VernacShow s ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@ vernac_show ~pstate s;
-    pstate
+    VtReadProofOpt(fun ~pstate ->
+      unsupported_attributes atts;
+      Feedback.msg_notice @@ vernac_show ~pstate s)
   | VernacCheckGuard ->
-    unsupported_attributes atts;
-    Feedback.msg_notice @@
-      vernac_require_open_proof ~pstate (vernac_check_guard);
-    pstate
+    VtReadProof(fun ~pstate ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_check_guard ~pstate)
   | VernacProof (tac, using) ->
+    VtModifyProof(fun ~pstate ->
     unsupported_attributes atts;
     let using = Option.append using (Proof_using.get_default_proof_using ()) in
     let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
     let usings = if Option.is_empty using then "using:no" else "using:yes" in
     Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
-    let pstate =
-      vernac_require_open_proof ~pstate (fun ~pstate ->
-          let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
-          Option.cata (vernac_set_used_variables ~pstate) pstate using)
-    in Some pstate
+    let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
+    Option.cata (vernac_set_used_variables ~pstate) pstate using)
   | VernacProofMode mn ->
-    unsupported_attributes atts;
-    pstate
+    VtDefault(fun () -> unsupported_attributes atts)
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
-    (* XXX: Here we are returning the state! :) *)
-    let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
-    st.Vernacstate.proof
+    Vernacextend.type_vernac ~atts opn args
+
+(* "locality" is the prefix "Local" attribute, while the "local" component
+ * is the outdated/deprecated "Local" attribute of some vernacular commands
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let rec interp_expr ?proof ~atts ~st c =
+  let pstate = st.Vernacstate.proof in
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+  match c with
+
+  (* The STM should handle that, but LOAD bypasses the STM... *)
+  | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
+  | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
+  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
+
+  (* Resetting *)
+  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
+  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
+  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
+  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
+
+  (* This one is possible to handle here *)
+  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
+
+  (* Loading a file requires access to the control interpreter so
+     [vernac_load] is mutually-recursive with [interp_expr] *)
+  | VernacLoad (verbosely,fname) ->
+    unsupported_attributes atts;
+    vernac_load ?proof ~verbosely ~st fname
+
+  (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
+  | VernacEndProof e ->
+    unsupported_attributes atts;
+    vernac_end_proof ?proof ?pstate e
+
+  | v ->
+    let fv = translate_vernac ~atts v in
+    interp_typed_vernac ~pstate fv
 
 (* XXX: This won't properly set the proof mode, as of today, it is
    controlled by the STM. Thus, we would need access information from
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 12451370c8..d94ddc1aaf 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,7 +42,11 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 (** Helper *)
-val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a
+val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a
+
+val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a
+
+val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 730f5fd6da..6f8a4e8a3c 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -53,14 +53,23 @@ type vernac_when =
   | VtLater
 type vernac_classification = vernac_type * vernac_when
 
-type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type typed_vernac =
+  | VtDefault of (unit -> unit)
+  | VtNoProof of (unit -> unit)
+  | VtCloseProof of (pstate:Proof_global.t -> unit)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
+
+type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 211 :
-    (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t)
+    (Vernacexpr.extend_name, bool * (plugin_args -> vernac_command)) Hashtbl.t)
 
 let vinterp_add depr s f =
   try
@@ -83,7 +92,7 @@ let warn_deprecated_command =
 
 (* Interpretation of a vernac command *)
 
-let call opn converted_args ~atts ~st =
+let type_vernac opn converted_args ~atts =
   let phase = ref "Looking up command" in
   try
     let depr, callback = vinterp_map opn in
@@ -99,7 +108,7 @@ let call opn converted_args ~atts ~st =
     phase := "Checking arguments";
     let hunk = callback converted_args in
     phase := "Executing command";
-    hunk ~atts ~st
+    hunk ~atts
   with
     | reraise ->
         let reraise = CErrors.push reraise in
@@ -125,7 +134,7 @@ let classify_as_sideeff = VtSideff [], VtLater
 let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
+| TyNil : (vernac_command, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
@@ -151,7 +160,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio
   end
 
 (** Stupid GADTs forces us to duplicate the definition just for typing *)
-let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_command = function
 | TyNil -> fun f args ->
   begin match args with
   | [] -> f
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index b37e527f47..60e371a6d9 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -71,18 +71,27 @@ type vernac_classification = vernac_type * vernac_when
 
 (** Interpretation of extended vernac phrases. *)
 
-type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type typed_vernac =
+  | VtDefault of (unit -> unit)
+  | VtNoProof of (unit -> unit)
+  | VtCloseProof of (pstate:Proof_global.t -> unit)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
+
+type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command
 
 (** {5 VERNAC EXTEND} *)
 
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
+| TyNil : (vernac_command, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 77f54361da..0fbde1ade5 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -30,10 +30,12 @@ end
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.t option; (* proof state *)
+  proof   : Proof_global.stack option; (* proof state *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
+let pstate st = Option.map Proof_global.get_current_pstate st.proof
+
 let s_cache = ref None
 let s_proof = ref None
 
@@ -96,17 +98,21 @@ module Proof_global = struct
     | None -> raise NoCurrentProof
     | Some x -> f x
 
+  let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
+
   let dd f = match !s_proof with
     | None -> raise NoCurrentProof
     | Some x -> s_proof := Some (f x)
 
+  let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
+
   let there_are_pending_proofs () = !s_proof <> None
-  let get_open_goals () = cc get_open_goals
+  let get_open_goals () = cc1 get_open_goals
 
-  let set_terminator x = dd (set_terminator x)
-  let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof
-  let give_me_the_proof () = cc give_me_the_proof
-  let get_current_proof_name () = cc get_current_proof_name
+  let set_terminator x = dd1 (set_terminator x)
+  let give_me_the_proof_opt () = Option.map (fun p -> give_me_the_proof (Proof_global.get_current_pstate p)) !s_proof
+  let give_me_the_proof () = cc1 give_me_the_proof
+  let get_current_proof_name () = cc1 get_current_proof_name
 
   let simple_with_current_proof f =
     dd (simple_with_current_proof f)
@@ -118,18 +124,18 @@ module Proof_global = struct
   let install_state s = s_proof := Some s
 
   let return_proof ?allow_partial () =
-    cc (return_proof ?allow_partial)
+    cc1 (return_proof ?allow_partial)
 
   let close_future_proof ~opaque ~feedback_id pf =
-    cc (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+    cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
-    cc (close_proof ~opaque ~keep_body_ucst_separate f)
+    cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
 
   let discard_all () = s_proof := None
-  let update_global_env () = dd update_global_env
+  let update_global_env () = dd1 update_global_env
 
-  let get_current_context () = cc Pfedit.get_current_context
+  let get_current_context () = cc1 Pfedit.get_current_context
 
   let get_all_proof_names () =
     try cc get_all_proof_names
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index dff81ad9bb..b0f3c572e5 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -21,10 +21,12 @@ end
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.t option; (* proof state *)
+  proof   : Proof_global.stack option; (* proof state *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
+val pstate : t -> Proof_global.t option
+
 val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit
 
@@ -39,11 +41,11 @@ module Proof_global : sig
   open Proof_global
 
   (* Low-level stuff *)
-  val get : unit -> t option
-  val set : t option -> unit
+  val get : unit -> stack option
+  val set : stack option -> unit
 
-  val freeze : marshallable:bool -> t option
-  val unfreeze : t -> unit
+  val freeze : marshallable:bool -> stack option
+  val unfreeze : stack -> unit
 
   exception NoCurrentProof
 
@@ -61,7 +63,7 @@ module Proof_global : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val install_state : t -> unit
+  val install_state : stack -> unit
 
   val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
 
@@ -79,7 +81,7 @@ module Proof_global : sig
 
   val get_all_proof_names : unit -> Names.Id.t list
 
-  val copy_terminators : src:t option -> tgt:t option -> t option
+  val copy_terminators : src:stack option -> tgt:stack option -> stack option
 
 end
 [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]