Merge PR#403: Split Vernacular Processing from Toplevel

5 files changed, 147 insertions, 772 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
deleted file mode 100644
index 55f33be399..0000000000
--- a/stm/lemmas.ml
+++ /dev/null
@@ -1,557 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Created by Hugo Herbelin from contents related to lemma proofs in
-   file command.ml, Aug 2009 *)
-
-open CErrors
-open Util
-open Flags
-open Pp
-open Names
-open Term
-open Declarations
-open Declareops
-open Entries
-open Environ
-open Nameops
-open Globnames
-open Decls
-open Decl_kinds
-open Declare
-open Pretyping
-open Termops
-open Namegen
-open Reductionops
-open Constrexpr
-open Constrintern
-open Impargs
-open Context.Rel.Declaration
-
-module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
-
-type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
-let mk_hook hook = hook
-let call_hook fix_exn hook l c =
-  try hook l c
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    iraise (fix_exn e)
-
-(* Support for mutually proved theorems *)
-
-let retrieve_first_recthm = function
-  | VarRef id ->
-      (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
-  | ConstRef cst ->
-      let cb = Global.lookup_constant cst in
-      (Global.body_of_constant_body cb, is_opaque cb)
-  | _ -> assert false
-
-let adjust_guardness_conditions const = function
-  | [] -> const (* Not a recursive statement *)
-  | possible_indexes ->
-  (* Try all combinations... not optimal *)
-     let env = Global.env() in
-     { const with const_entry_body =
-        Future.chain ~greedy:true ~pure:true const.const_entry_body
-        (fun ((body, ctx), eff) ->
-          match kind_of_term body with
-          | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-(*      let possible_indexes =
-	List.map2 (fun i c -> match i with Some i -> i | None ->
-	  List.interval 0 (List.length ((lam_assum c))))
-	  lemma_guard (Array.to_list fixdefs) in
-*)
-              let add c cb e =
-                let exists c e =
-                  try ignore(Environ.lookup_constant c e); true
-                  with Not_found -> false in 
-                if exists c e then e else Environ.add_constant c cb e in
-              let env = List.fold_left (fun env { eff } ->
-                match eff with
-                | SEsubproof (c, cb,_) -> add c cb env
-                | SEscheme (l,_) ->
-                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
-                env (Safe_typing.side_effects_of_private_constants eff) in
-              let indexes =
-                search_guard Loc.ghost env
-                  possible_indexes fixdecls in
-		(mkFix ((indexes,0),fixdecls), ctx), eff
-          | _ -> (body, ctx), eff) }
-
-let find_mutually_recursive_statements thms =
-    let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls,annot)) ->
-      let (hyps,ccl) = decompose_prod_assum t in
-      let x = (id,(t,impls)) in
-      match annot with
-      (* Explicit fixpoint decreasing argument is given *)
-      | Some (Some (_,id),CStructRec) ->
-          let i,b,typ = lookup_rel_id id hyps in
-          (match kind_of_term t with
-          | Ind ((kn,_ as ind), u) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
-              [ind,x,i],[]
-          | _ ->
-              error "Decreasing argument is not an inductive assumption.")
-      (* Unsupported cases *)
-      | Some (_,(CWfRec _|CMeasureRec _)) ->
-          error "Only structural decreasing is supported for mutual statements."
-      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
-      | None | Some (None, CStructRec) ->
-      let whnf_hyp_hds = map_rel_context_in_env
-        (fun env c -> fst (whd_all_stack env Evd.empty c))
-        (Global.env()) hyps in
-      let ind_hyps =
-        List.flatten (List.map_i (fun i decl ->
-          let t = RelDecl.get_type decl in
-          match kind_of_term t with
-          | Ind ((kn,_ as ind),u) when
-                let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
-              [ind,x,i]
-          | _ ->
-              []) 0 (List.rev whnf_hyp_hds)) in
-      let ind_ccl =
-        let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
-        match kind_of_term whnf_ccl with
-        | Ind ((kn,_ as ind),u) when
-              let mind = Global.lookup_mind kn in
-              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
-            [ind,x,0]
-        | _ ->
-            [] in
-      ind_hyps,ind_ccl) thms in
-    let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
-    (* Check if all conclusions are coinductive in the same type *)
-    (* (degenerated cartesian product since there is at most one coind ccl) *)
-    let same_indccl =
-      List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] ind_ccls in
-    let ordered_same_indccl =
-      List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
-    (* Check if some hypotheses are inductive in the same type *)
-    let common_same_indhyp =
-      List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] inds_hyps in
-    let ordered_inds,finite,guard =
-      match ordered_same_indccl, common_same_indhyp with
-      | indccl::rest, _ ->
-	  assert (List.is_empty rest);
-          (* One occ. of common coind ccls and no common inductive hyps *)
-	  if not (List.is_empty common_same_indhyp) then
-	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
-	  flush_all ();
-          indccl, true, []
-      | [], _::_ ->
-          let () = match same_indccl with
-          | ind :: _ ->
-            if List.distinct_f ind_ord (List.map pi1 ind)
-            then
-              if_verbose Feedback.msg_info
-                (strbrk
-                   ("Coinductive statements do not follow the order of "^
-                    "definition, assuming the proof to be by induction."));
-            flush_all ()
-          | _ -> ()
-          in
-          let possible_guards = List.map (List.map pi3) inds_hyps in
-	  (* assume the largest indices as possible *)
-	  List.last common_same_indhyp, false, possible_guards
-      | _, [] ->
-	  error
-            ("Cannot find common (mutual) inductive premises or coinductive" ^
-             " conclusions in the statements.")
-    in
-    (finite,guard,None), ordered_inds
-
-let look_for_possibly_mutual_statements = function
-  | [id,(t,impls,None)] ->
-      (* One non recursively proved theorem *)
-      None,[id,(t,impls)],None
-  | _::_ as thms ->
-    (* More than one statement and/or an explicit decreasing mark: *)
-    (* we look for a common inductive hyp or a common coinductive conclusion *)
-    let recguard,ordered_inds = find_mutually_recursive_statements thms in
-    let thms = List.map pi2 ordered_inds in
-    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
-  | [] -> anomaly (Pp.str "Empty list of theorems.")
-
-(* Saving a goal *)
-
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
-  try
-    let const = adjust_guardness_conditions const do_guard in
-    let k = Kindops.logical_kind_of_goal_kind kind in
-    let l,r = match locality with
-      | Discharge when Lib.sections_are_opened () ->
-          let c = SectionLocalDef const in
-          let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Local, VarRef id)
-      | Local | Global | Discharge ->
-          let local = match locality with
-          | Local | Discharge -> true
-          | Global -> false
-          in
-          let kn =
-           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
-          (locality, ConstRef kn) in
-    definition_message id;
-    Option.iter (Universes.register_universe_binders r) pl;
-    call_hook (fun exn -> exn) hook l r
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    iraise (fix_exn e)
-
-let default_thm_id = Id.of_string "Unnamed_thm"
-
-let compute_proof_name locality = function
-  | Some ((loc,id),pl) ->
-      (* We check existence here: it's a bit late at Qed time *)
-      if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
-	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
-      then
-        user_err ~loc  (pr_id id ++ str " already exists.");
-      id, pl
-  | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
-
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
-  let t_i = norm t_i in
-  match body with
-  | None ->
-      (match locality with
-      | Discharge ->
-          let impl = false in (* copy values from Vernacentries *)
-          let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (Discharge, VarRef id,imps)
-      | Local | Global ->
-          let k = IsAssumption Conjectural in
-          let local = match locality with
-          | Local -> true
-          | Global -> false
-          | Discharge -> assert false
-          in
-          let ctx = Univ.ContextSet.to_context ctx in
-          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
-          let kn = declare_constant id ~local decl in
-          (locality,ConstRef kn,imps))
-  | Some body ->
-      let body = norm body in
-      let k = Kindops.logical_kind_of_goal_kind kind in
-      let rec body_i t = match kind_of_term t with
-        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-        | CoFix (0,decls) -> mkCoFix (i,decls)
-        | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
-        | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
-        | App (t, args) -> mkApp (body_i t, args)
-        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
-      let body_i = body_i body in
-      match locality with
-      | Discharge ->
-          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
-	  let c = SectionLocalDef const in
-	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Discharge,VarRef id,imps)
-      | Local | Global ->
-        let ctx = Univ.ContextSet.to_context ctx in
-        let local = match locality with
-        | Local -> true
-        | Global -> false
-        | Discharge -> assert false
-        in
-        let const =
-	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
-	in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        (locality,ConstRef kn,imps)
-
-let save_hook = ref ignore
-let set_save_hook f = save_hook := f
-
-let save_named ?export_seff proof =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs pl do_guard persistence hook
-
-let check_anonymity id save_ident =
-  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
-    error "This command can only be used for unnamed theorem."
-
-let save_anonymous ?export_seff proof save_ident =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs pl do_guard persistence hook
-
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,(cstrs,pl),do_guard,_,hook = proof in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs pl do_guard
-      (Global, const.const_entry_polymorphic, Proof kind) hook
-
-(* Admitted *)
-
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
-                                spc () ++ strbrk "declared as an axiom.")
-
-let admit (id,k,e) pl hook () =
-  let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
-  let () = match k with
-  | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
-  in
-  let () = assumption_message id in
-  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
-  call_hook (fun exn -> exn) hook Global (ConstRef kn)
-
-(* Starting a goal *)
-
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-
-let get_proof proof do_guard hook opacity =
-  let (id,(const,univs,persistence)) =
-    Pfedit.cook_this_proof proof
-  in
-  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-
-let check_exist =
-  List.iter (fun (loc,id) ->
-    if not (Nametab.exists_cci (Lib.make_path id)) then
-        user_err ~loc  (pr_id id ++ str " does not exist.")
-  )
-
-let universe_proof_terminator compute_guard hook =
-  let open Proof_global in
-  make_terminator begin function
-  | Admitted (id,k,pe,(ctx,pl)) ->
-      admit (id,k,pe) pl (hook (Some ctx)) ();
-      Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt,proof) ->
-      let is_opaque, export_seff, exports = match opaque with
-        | Vernacexpr.Transparent -> false, true, []
-        | Vernacexpr.Opaque None -> true, false, []
-        | Vernacexpr.Opaque (Some l) -> true, true, l in
-      let proof = get_proof proof compute_guard
-	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
-      begin match idopt with
-      | None -> save_named ~export_seff proof
-      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
-      | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength ~export_seff proof kind id
-      end;
-      check_exist exports
-  end
-
-let standard_proof_terminator compute_guard hook =
-  universe_proof_terminator compute_guard (fun _ -> hook)
-
-let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
-  in
-  let sign = 
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
-  !start_hook c;
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = match terminator with
-  | None -> universe_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
-  in
-  let sign = 
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
-  !start_hook c;
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let rec_tac_initializer finite guard thms snl =
-  if finite then
-    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
-    | (id,_)::l -> Tactics.mutual_cofix id l 0
-    | _ -> assert false
-  else
-    (* nl is dummy: it will be recomputed at Qed-time *)
-    let nl = match snl with 
-     | None -> List.map succ (List.map List.last guard)
-     | Some nl -> nl
-    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
-       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
-       | _ -> assert false
-
-let start_proof_with_initialization kind ctx recguard thms snl hook =
-  let intro_tac (_, (_, (ids, _))) =
-    Tacticals.New.tclMAP (function
-    | Name id -> Tactics.intro_mustbe_force id
-    | Anonymous -> Tactics.intro) (List.rev ids) in
-  let init_tac,guard = match recguard with
-  | Some (finite,guard,init_tac) ->
-      let rec_tac = rec_tac_initializer finite guard thms snl in
-      Some (match init_tac with
-        | None -> 
-            if Flags.is_auto_intros () then 
-              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
-            else
-              rec_tac
-        | Some tacl ->
-            Tacticals.New.tclTHENS rec_tac
-            (if Flags.is_auto_intros () then
-              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
-            else
-              tacl)),guard
-  | None ->
-      let () = match thms with [_] -> () | _ -> assert false in
-      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
-  match thms with
-  | [] -> anomaly (Pp.str "No proof to start")
-  | ((id,pl),(t,(_,imps)))::other_thms ->
-      let hook ctx strength ref =
-        let ctx = match ctx with
-        | None -> Evd.empty_evar_universe_context
-        | Some ctx -> ctx
-        in
-        let other_thms_data =
-          if List.is_empty other_thms then [] else
-            (* there are several theorems defined mutually *)
-            let body,opaq = retrieve_first_recthm ref in
-            let subst = Evd.evar_universe_context_subst ctx in
-            let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = UState.context_set (*FIXME*) ctx in
-	    let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
-        let thms_data = (strength,ref,imps)::other_thms_data in
-        List.iter (fun (strength,ref,imps) ->
-	  maybe_declare_manual_implicits false ref imps;
-	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
-
-let start_proof_com ?inference_hook kind thms hook =
-  let env0 = Global.env () in
-  let levels = Option.map snd (fst (List.hd thms)) in 
-  let evdref = ref (match levels with
-		    | None -> Evd.from_env env0
-		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
-  in
-  let thms = List.map (fun (sopt,(bl,t,guard)) ->
-    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
-    let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    let flags = all_and_fail_flags in
-    let flags = { flags with use_hook = inference_hook } in
-    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
-    let ids = List.map RelDecl.get_name ctx in
-      (compute_proof_name (pi1 kind) sopt,
-      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
-    thms in
-  let recguard,thms,snl = look_for_possibly_mutual_statements thms in
-  let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-  let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  let () =
-    match levels with
-    | None -> ()
-    | Some l -> ignore (Evd.universe_context evd ?names:l)
-  in
-  let evd =
-    if pi2 kind then evd
-    else (* We fix the variables to ensure they won't be lowered to Set *)
-      Evd.fix_undefined_variables evd
-  in
-    start_proof_with_initialization kind evd recguard thms snl hook
-
-
-(* Saving a proof *)
-
-let keep_admitted_vars = ref true
-
-let _ =
-  let open Goptions in
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "keep section variables in admitted proofs";
-      optkey   = ["Keep"; "Admitted"; "Variables"];
-      optread  = (fun () -> !keep_admitted_vars);
-      optwrite = (fun b -> keep_admitted_vars := b) }
-
-let save_proof ?proof = function
-  | Vernacexpr.Admitted ->
-      let pe =
-        let open Proof_global in
-        match proof with
-        | Some ({ id; entries; persistence = k; universes }, _) ->
-            if List.length entries <> 1 then
-              error "Admitted does not support multiple statements";
-            let { const_entry_secctx; const_entry_type } = List.hd entries in
-            if const_entry_type = None then
-              error "Admitted requires an explicit statement";
-            let typ = Option.get const_entry_type in
-            let ctx = Evd.evar_context_universe_context (fst universes) in
-            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
-        | None ->
-            let pftree = Pfedit.get_pftreestate () in
-            let id, k, typ = Pfedit.current_proof_statement () in
-            let universes = Proof.initial_euctx pftree in
-            (* This will warn if the proof is complete *)
-            let pproofs, _univs =
-              Proof_global.return_proof ~allow_partial:true () in
-            let sec_vars =
-              if not !keep_admitted_vars then None
-              else match  Pfedit.get_used_variables(), pproofs with
-              | Some _ as x, _ -> x
-              | None, (pproof, _) :: _ -> 
-                  let env = Global.env () in
-                  let ids_typ = Environ.global_vars_set env typ in
-                  let ids_def = Environ.global_vars_set env pproof in
-                  Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
-              | _ -> None in
-	    let names = Pfedit.get_universe_binders () in
-            let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.universe_context ?names evd in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
-		     (universes, Some binders))
-      in
-      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
-  | Vernacexpr.Proved (is_opaque,idopt) ->
-      let (proof_obj,terminator) =
-        match proof with
-        | None ->
-            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
-        | Some proof -> proof
-      in
-      (* if the proof is given explicitly, nothing has to be deleted *)
-      if Option.is_empty proof then Pfedit.delete_current_proof ();
-      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
-
-(* Miscellaneous *)
-
-let get_current_context () =
-  Pfedit.get_current_context ()
-           
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
deleted file mode 100644
index 39c089be9f..0000000000
--- a/stm/lemmas.mli
+++ /dev/null
@@ -1,69 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Decl_kinds
-open Pfedit
-
-type 'a declaration_hook
-val mk_hook :
-  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
-
-val call_hook :
-  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
-
-(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
-
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-   unit declaration_hook -> unit
-
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
-
-val start_proof_com :
-  ?inference_hook:Pretyping.inference_hook ->
-  goal_kind -> Vernacexpr.proof_expr list ->
-  unit declaration_hook -> unit
-
-val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_map ->
-  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t * universe_binders option) *
-     (types * (Name.t list * Impargs.manual_explicitation list))) list
-  -> int list option -> unit declaration_hook -> unit
-
-val universe_proof_terminator :
-  Proof_global.lemma_possible_guards ->
-    (Evd.evar_universe_context option -> unit declaration_hook) ->
-    Proof_global.proof_terminator
-
-val standard_proof_terminator :
-  Proof_global.lemma_possible_guards -> unit declaration_hook ->
-    Proof_global.proof_terminator
-
-(** {6 ... } *)
-
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
-
-val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
-
-(** [get_current_context ()] returns the evar context and env of the
-   current open proof if any, otherwise returns the empty evar context
-   and the current global env *)
-
-val get_current_context : unit -> Evd.evar_map * Environ.env
diff --git a/stm/stm.ml b/stm/stm.ml
index 6f34c8dbc3..e698d1c72e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -24,11 +24,13 @@ open Ppvernac
 open Vernac_classifier
 open Feedback
 
+let execution_error state_id loc msg =
+    feedback ~id:(State state_id)
+      (Message (Error, Some loc, pp_to_richpp msg))
+
 module Hooks = struct
 
 let process_error, process_error_hook = Hook.make ()
-let interp, interp_hook = Hook.make ()
-let with_fail, with_fail_hook = Hook.make ()
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
@@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make
  ~default:(fun id loc msg ->
         feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
 
-let execution_error, execution_error_hook = Hook.make
- ~default:(fun state_id loc msg ->
-    feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
-
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
@@ -105,26 +103,6 @@ let may_pierce_opaque = function
   | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
   | _ -> false
 
-(* Wrapper for Vernacentries.interp to set the feedback id *)
-let vernac_interp ?proof id ?route { verbose; loc; expr } =
-  let rec internal_command = function
-    | VernacResetName _ | VernacResetInitial | VernacBack _
-    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
-    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
-    | _ -> false in
-  if internal_command expr then begin
-    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
-  end else begin
-    set_id_for_feedback ?route (State id);
-    Aux_file.record_in_aux_set_at loc;
-    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
-    try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
-    with e ->
-      let e = CErrors.push e in
-      iraise Hooks.(call_process_error_once e)
-  end
-
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
 let indentation_of_string s =
   let len = String.length s in
@@ -860,7 +838,7 @@ end = struct (* {{{ *)
     | None ->
         let loc = Option.default Loc.ghost (Loc.get_loc info) in
         let (e, info) = Hooks.(call_process_error_once (e, info)) in
-        Hooks.(call execution_error id loc (iprint (e, info)));
+        execution_error id loc (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
   let same_env { system = s1 } { system = s2 } =
@@ -910,6 +888,126 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
+(* indentation code for Show Script, initially contributed
+ * by D. de Rauglaudre. Should be moved away.
+ *)
+
+module ShowScript = struct
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+  (* ng1 : number of goals remaining at the current level (before cmd)
+     ngl1 : stack of previous levels with their remaining goals
+     ng : number of goals after the execution of cmd
+     beginend : special indentation stack for { } *)
+  let ngprev = List.fold_left (+) ng1 ngl1 in
+  let new_ngl =
+    if ng > ngprev then
+      (* We've branched *)
+      (ng - ngprev + 1, ng1 - 1 :: ngl1)
+    else if ng < ngprev then
+      (* A subgoal have been solved. Let's compute the new current level
+	 by discarding all levels with 0 remaining goals. *)
+      let rec loop = function
+	| (0, ng2::ngl2) -> loop (ng2,ngl2)
+	| p -> p
+      in loop (ng1-1, ngl1)
+    else
+      (* Standard case, same goal number as before *)
+      (ng1, ngl1)
+  in
+  (* When a subgoal have been solved, separate this block by an empty line *)
+  let new_nl = (ng < ngprev)
+  in
+  (* Indentation depth *)
+  let ind = List.length ngl1
+  in
+  (* Some special handling of bullets and { }, to get a nicer display *)
+  let pred n = max 0 (n-1) in
+  let ind, nl, new_beginend = match cmd with
+    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+    | VernacBullet _ -> pred ind, nl, beginend
+    | _ -> ind, nl, beginend
+  in
+  let pp =
+    (if nl then fnl () else mt ()) ++
+    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
+  in
+  (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let get_script prf =
+  let branch, test =
+    match prf with
+    | None -> VCS.Branch.master, fun _ -> true
+    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
+  let rec find acc id =
+    if Stateid.equal id Stateid.initial ||
+       Stateid.equal id Stateid.dummy then acc else
+    let view = VCS.visit id in
+    match view.step with
+    | `Fork((_,_,_,ns), _) when test ns -> acc
+    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+    | `Sideff (`Ast (x,_)) ->
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+    | `Sideff (`Id id)  -> find acc id
+    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd _ -> find acc view.next
+    | `Alias (id,_) -> find acc id
+    | `Fork _ -> find acc view.next
+    in
+  find [] (VCS.get_branch_pos branch)
+
+let show_script ?proof () =
+  try
+    let prf =
+      try match proof with
+      | None -> Some (Pfedit.get_current_proof_name ())
+      | Some (p,_) -> Some (p.Proof_global.id)
+      with Proof_global.NoCurrentProof -> None
+    in
+    let cmds = get_script prf in
+    let _,_,_,indented_cmds =
+      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+    in
+    let indented_cmds = List.rev (indented_cmds) in
+    msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+  with Vcs_aux.Expired -> ()
+
+end
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+(* It is currently called 19 times, this number should be certainly
+   reduced... *)
+let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
+  (* The Stm will gain the capability to interpret commmads affecting
+     the whole document state, such as backtrack, etc... so we start
+     to design the stm command interpreter now *)
+  set_id_for_feedback ?route (State id);
+  Aux_file.record_in_aux_set_at loc;
+  (* We need to check if a command should be filtered from
+   * vernac_entries, as it cannot handle it. This should go away in
+   * future refactorings.
+   *)
+  let rec is_filtered_command = function
+  | VernacResetName _ | VernacResetInitial | VernacBack _
+  | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+  | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+  | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
+  | _ -> false
+  in
+  let aux_interp cmd =
+  if is_filtered_command cmd then
+    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+  else match cmd with
+  | VernacShow ShowScript -> ShowScript.show_script ()
+  | expr ->
+    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+    try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
+    with e ->
+      let e = CErrors.push e in
+      iraise Hooks.(call_process_error_once e)
+  in aux_interp expr
 
 (****************************** CRUFT *****************************************)
 (******************************************************************************)
@@ -1287,7 +1385,7 @@ end = struct (* {{{ *)
         let info = Stateid.add ~valid:start Exninfo.null start in
         let e = (RemoteException (strbrk s), info) in
         t_assign (`Exn e);
-        Hooks.(call execution_error start Loc.ghost (strbrk s));
+        execution_error start Loc.ghost (strbrk s);
         feedback (InProgress ~-1)
 
   let build_proof_here ~drop_pt (id,valid) loc eop =
@@ -1321,7 +1419,7 @@ end = struct (* {{{ *)
             Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
-          vernac_interp stop
+          stm_vernac_interp stop
             ~proof:(pobject, terminator)
             { verbose = false; loc; indentation = 0; strlen = 0;
               expr = (VernacEndProof (Proved (Opaque None,None))) }) in
@@ -1463,7 +1561,7 @@ end = struct (* {{{ *)
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~cache:`No start;
-      vernac_interp stop ~proof
+      stm_vernac_interp stop ~proof
         { verbose = false; loc; indentation = 0; strlen = 0;
           expr = (VernacEndProof (Proved (Opaque None,None))) };
       `OK proof
@@ -1714,7 +1812,7 @@ end = struct (* {{{ *)
        else begin
         let (i, ast) = r_ast in
         Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
-        vernac_interp r_state_fb ast;
+        stm_vernac_interp r_state_fb ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
@@ -1750,7 +1848,7 @@ end = struct (* {{{ *)
         | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
         | _ -> e, time, fail in find false false e in
-    Hooks.call Hooks.with_fail fail (fun () ->
+    Vernacentries.with_fail fail (fun () ->
     (if time then System.with_time false else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
@@ -1843,7 +1941,7 @@ end = struct (* {{{ *)
     VCS.print ();
     Reach.known_state ~cache:`No r_where;
     try
-      vernac_interp r_for { r_what with verbose = true };
+      stm_vernac_interp r_for { r_what with verbose = true };
       feedback ~id:(State r_for) Processed
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
@@ -2052,7 +2150,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                Proof_global.with_current_proof (fun _ p ->
                  feedback ~id:(State id) Feedback.AddedAxiom;
                  fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
-               Option.iter (fun expr -> vernac_interp id {
+               Option.iter (fun expr -> stm_vernac_interp id {
                   verbose = true; loc = Loc.ghost; expr; indentation = 0;
                   strlen = 0 })
                recovery_command
@@ -2131,24 +2229,24 @@ let known_state ?(redefine_qed=false) ~cache id =
             resilient_tactic id cblock (fun () ->
               reach view.next;
               Hooks.(call tactic_being_run true); 
-              vernac_interp id x;
+              stm_vernac_interp id x;
               Hooks.(call tactic_being_run false)); 
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
             resilient_command reach view.next;
-            vernac_interp id x;
+            stm_vernac_interp id x;
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
-            vernac_interp id x;
+            stm_vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
       | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
             reach ~cache:`Shallow prev;
             reach view.next;
-            (try vernac_interp id x;
+            (try stm_vernac_interp id x;
             with e when CErrors.noncritical e ->
               let (e, info) = CErrors.push e in
               let info = Stateid.add info ~valid:prev id in
@@ -2198,14 +2296,14 @@ let known_state ?(redefine_qed=false) ~cache id =
                       Proof_global.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
-                    vernac_interp id ~proof x;
+                    stm_vernac_interp id ~proof x;
                     feedback ~id:(State id) Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
               ), (if redefine_qed then `No else `Yes), true
           | `Sync (name, _, `Immediate) -> (fun () -> 
-                reach eop; vernac_interp id x; Proof_global.discard_all ()
+                reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
               ), `Yes, true
           | `Sync (name, pua, reason) -> (fun () ->
                 log_processing_sync id name reason;
@@ -2226,7 +2324,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 if keep != VtKeepAsAxiom then
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
-                vernac_interp id ?proof x;
+                stm_vernac_interp id ?proof x;
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at x.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
@@ -2242,7 +2340,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
       | `Sideff (`Ast (x,_)) -> (fun () ->
-            reach view.next; vernac_interp id x; update_global_env ()
+            reach view.next; stm_vernac_interp id x; update_global_env ()
           ), cache, true
       | `Sideff (`Id origin) -> (fun () ->
             reach view.next;
@@ -2430,7 +2528,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
       (* PG stuff *)    
-      | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
+      | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok
       | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
       (* Joining various parts of the document *)
       | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
@@ -2474,13 +2572,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       (* Query *)
       | VtQuery (false,(report_id,route)), VtNow when tty = true ->
           finish ();
-          (try Future.purify (vernac_interp report_id ~route)
+          (try Future.purify (stm_vernac_interp report_id ~route)
             {x with verbose = true }
            with e when CErrors.noncritical e ->
              let e = CErrors.push e in
              iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
       | VtQuery (false,(report_id,route)), VtNow ->
-          (try vernac_interp report_id ~route x
+          (try stm_vernac_interp report_id ~route x
            with e ->
              let e = CErrors.push e in
              iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
@@ -2553,7 +2651,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           
       (* Side effect on all branches *)
       | VtUnknown, _ when expr = VernacToplevelControl Drop ->
-          vernac_interp (VCS.get_branch_pos head) x; `Ok
+          stm_vernac_interp (VCS.get_branch_pos head) x; `Ok
 
       | VtSideff l, w ->
           let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
@@ -2579,7 +2677,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
             VCS.checkout VCS.Branch.master;
             let mid = VCS.get_branch_pos VCS.Branch.master in
             Reach.known_state ~cache:(interactive ()) mid;
-            vernac_interp id x;
+            stm_vernac_interp id x;
             (* Vernac x may or may not start a proof *)
             if not in_proof && Proof_global.there_are_pending_proofs () then
             begin
@@ -2609,7 +2707,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
     begin match expr with 
       | VernacStm (PGLast _) ->
         if not (VCS.Branch.equal head VCS.Branch.master) then
-          vernac_interp Stateid.dummy
+          stm_vernac_interp Stateid.dummy
             { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
               expr = VernacShow (ShowGoal OpenSubgoals) }
       | _ -> ()
@@ -2856,102 +2954,13 @@ let proofname b = match VCS.get_branch b with
 let get_all_proof_names () =
   List.map unmangle (List.map_filter proofname (VCS.branches ()))
 
-let get_current_proof_name () =
-  Option.map unmangle (proofname (VCS.current_branch ()))
-
-let get_script prf =
-  let branch, test =
-    match prf with
-    | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
-  let rec find acc id =
-    if Stateid.equal id Stateid.initial ||
-       Stateid.equal id Stateid.dummy then acc else
-    let view = VCS.visit id in
-    match view.step with
-    | `Fork((_,_,_,ns), _) when test ns -> acc
-    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
-    | `Sideff (`Ast (x,_)) ->
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
-    | `Sideff (`Id id)  -> find acc id
-    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
-    | `Cmd _ -> find acc view.next
-    | `Alias (id,_) -> find acc id
-    | `Fork _ -> find acc view.next
-    in
-  find [] (VCS.get_branch_pos branch)
-
-(* indentation code for Show Script, initially contributed
-   by D. de Rauglaudre *)
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
-  (* ng1 : number of goals remaining at the current level (before cmd)
-     ngl1 : stack of previous levels with their remaining goals
-     ng : number of goals after the execution of cmd
-     beginend : special indentation stack for { } *)
-  let ngprev = List.fold_left (+) ng1 ngl1 in
-  let new_ngl =
-    if ng > ngprev then
-      (* We've branched *)
-      (ng - ngprev + 1, ng1 - 1 :: ngl1)
-    else if ng < ngprev then
-      (* A subgoal have been solved. Let's compute the new current level
-	 by discarding all levels with 0 remaining goals. *)
-      let rec loop = function
-	| (0, ng2::ngl2) -> loop (ng2,ngl2)
-	| p -> p
-      in loop (ng1-1, ngl1)
-    else
-      (* Standard case, same goal number as before *)
-      (ng1, ngl1)
-  in
-  (* When a subgoal have been solved, separate this block by an empty line *)
-  let new_nl = (ng < ngprev)
-  in
-  (* Indentation depth *)
-  let ind = List.length ngl1
-  in
-  (* Some special handling of bullets and { }, to get a nicer display *)
-  let pred n = max 0 (n-1) in
-  let ind, nl, new_beginend = match cmd with
-    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
-    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
-    | VernacBullet _ -> pred ind, nl, beginend
-    | _ -> ind, nl, beginend
-  in
-  let pp =
-    (if nl then fnl () else mt ()) ++
-    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
-  in
-  (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let show_script ?proof () =
-  try
-    let prf =
-      try match proof with
-      | None -> Some (Pfedit.get_current_proof_name ())
-      | Some (p,_) -> Some (p.Proof_global.id)
-      with Proof_global.NoCurrentProof -> None
-    in
-    let cmds = get_script prf in
-    let _,_,_,indented_cmds =
-      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
-    in
-    let indented_cmds = List.rev (indented_cmds) in
-    msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
-  with Vcs_aux.Expired -> ()
-
 (* Export hooks *)
 let state_computed_hook = Hooks.state_computed_hook
 let state_ready_hook = Hooks.state_ready_hook
 let parse_error_hook = Hooks.parse_error_hook
-let execution_error_hook = Hooks.execution_error_hook
 let forward_feedback_hook = Hooks.forward_feedback_hook
 let process_error_hook = Hooks.process_error_hook
-let interp_hook = Hooks.interp_hook
-let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
-let get_fix_exn () = !State.fix_exn_ref
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
 let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index b8a2a38596..0f0a3c4e13 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -184,7 +184,6 @@ val register_proof_block_delimiter :
 val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
@@ -213,12 +212,6 @@ val interp : bool -> vernac_expr located -> unit
 (* Queries for backward compatibility *)
 val current_proof_depth : unit -> int
 val get_all_proof_names : unit -> Id.t list
-val get_current_proof_name : unit -> Id.t option
-val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
 
 (* Hooks to be set by other Coq components in order to break file cycles *)
 val process_error_hook : Future.fix_exn Hook.t
-val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
-  Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
-val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
-val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 939ee187ae..4b254e8113 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,7 +4,6 @@ Vcs
 TQueue
 WorkerPool
 Vernac_classifier
-Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
 Stm