Merge branch 'trunk' into pr379

11 files changed, 228 insertions, 848 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 8acc3c233a..1254919880 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,9 +10,9 @@ open CErrors
 open Pp
 open Util
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
 type 'a worker_status = [ `Fresh | `Old of 'a ]
 
@@ -147,23 +147,23 @@ module Make(T : Task) = struct
     let stop_waiting = ref false in
     let expiration_date = ref (ref false) in
     let pick_task () =
-      prerr_endline "waiting for a task";
+      stm_prerr_endline "waiting for a task";
       let pick age (t, c) = not !c && T.task_match age t in
       let task, task_expiration =
         TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
       expiration_date := task_expiration;
       last_task := Some task;
-      prerr_endline ("got task: "^T.name_of_task task);
+      stm_prerr_endline ("got task: " ^ T.name_of_task task);
       task in
     let add_tasks l =
       List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
     let get_exec_token () =
       ignore(CoqworkmgrApi.get 1);
       got_token := true;
-      prerr_endline ("got execution token") in
+      stm_prerr_endline ("got execution token") in
     let kill proc =
       Worker.kill proc;
-      prerr_endline ("Worker exited: " ^
+      stm_prerr_endline ("Worker exited: " ^
         match Worker.wait proc with
         | Unix.WEXITED 0x400 -> "exit code unavailable"
         | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
       report_status ~id "Idle";
       let task = pick_task () in
       match T.request_of_task !worker_age task with
-      | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+      | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
       | Some req ->
       try
         get_exec_token ();
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
           raise e (* we pass the exception to the external handler *)
       | MarshalError s -> T.on_marshal_error s task; raise Die
       | e ->
-          pr_err ("Uncaught exception in worker manager: "^
-            string_of_ppcmds (print e));
+          stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
           flush_all (); raise Die
     done with
     | (Die | TQueue.BeingDestroyed) ->
@@ -261,7 +260,7 @@ module Make(T : Task) = struct
   let broadcast { queue } = TQueue.broadcast queue
 
   let enqueue_task { queue; active } (t, _ as item) =
-    prerr_endline ("Enqueue task "^T.name_of_task t);
+    stm_prerr_endline ("Enqueue task "^T.name_of_task t);
     TQueue.push queue item
 
   let cancel_worker { active } n = Pool.cancel n active
@@ -298,18 +297,11 @@ module Make(T : Task) = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
-  let pp_pid pp = 
-    (* Breaking all abstraction barriers... very nice *)
-    let get_xml pp = match Richpp.repr pp with
-      | Xml_datatype.Element("_", [], xml) -> xml
-      | _ -> assert false in
-    Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
-      get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
-      get_xml pp))
+  let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp)
 
   let debug_with_pid = Feedback.(function
     | { contents = Message(Debug, loc, pp) } as fb ->
-       { fb with contents = Message(Debug,loc,pp_pid pp) }
+       { fb with contents = Message(Debug,loc, pp_pid pp) }
     | x -> x)
 
   let main_loop () =
@@ -317,7 +309,6 @@ module Make(T : Task) = struct
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Feedback.set_logger Feedback.feedback_logger;
     (* We ask master to allocate universe identifiers *)
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
@@ -337,11 +328,11 @@ module Make(T : Task) = struct
         CEphemeron.clear ()
       with
       | MarshalError s ->
-        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+        stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
       | End_of_file ->
-        prerr_endline "connection lost"; flush_all (); exit 2
+        stm_prerr_endline "connection lost"; flush_all (); exit 2
       | e ->
-        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
         flush_all (); exit 1
     done
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
deleted file mode 100644
index 77fb960e16..0000000000
--- a/stm/lemmas.ml
+++ /dev/null
@@ -1,558 +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 -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr 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 (EConstr.of_constr ccl) in
-        match kind_of_term (EConstr.Unsafe.to_constr 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,EConstr.of_constr 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, EConstr.of_constr 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 (EConstr.of_constr 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,
-      (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.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 typ = EConstr.Unsafe.to_constr typ 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 681413a297..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 : (EConstr.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 -> EConstr.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 -> EConstr.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/proofworkertop.ml b/stm/proofworkertop.ml
index 23538a467e..0d2f9cb747 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index fff6d55434..9d30473739 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/stm.ml b/stm/stm.ml
index c1d1aa445d..b8a4064306 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,14 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s  = Printf.eprintf "%s] %s\n"     (System.process_id ()) s; flush stderr
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
 
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
-(* Opening ppvernac below aliases Richpp, see PR#185 *)
-let pp_to_richpp  = Richpp.richpp_of_pp
-let str_to_richpp = Richpp.richpp_of_string
+let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else ()
 
 open Vernacexpr
 open CErrors
@@ -24,11 +23,13 @@ open Ppvernac
 open Vernac_classifier
 open Feedback
 
+let execution_error state_id loc msg =
+    feedback ~id:(State state_id)
+      (Message (Error, Some loc, 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 ->
@@ -46,11 +47,7 @@ let forward_feedback, forward_feedback_hook =
 
 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))) ()
+        feedback ~id (Message(Error, Some loc, msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
@@ -105,26 +102,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
@@ -566,7 +543,7 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline (fun () -> "mode:" ^ mode);
+        stm_prerr_endline (fun () -> "mode:" ^ mode);
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
@@ -860,7 +837,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 } =
@@ -878,7 +855,7 @@ end = struct (* {{{ *)
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
     try
-      prerr_endline (fun () -> "defining "^str_id^" (cache="^
+      stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -886,7 +863,7 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline (fun () -> "setting cur id to "^str_id);
+      stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
@@ -910,6 +887,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
+    stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr)
+  else match cmd with
+  | VernacShow ShowScript -> ShowScript.show_script ()
+  | expr ->
+    stm_pperr_endline Pp.(fun () -> str "interpreting " ++ 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 +1384,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 +1418,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
@@ -1337,11 +1434,10 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline (fun () -> "failed with the following exception:");
-        prerr_endline (fun () -> string_of_ppcmds e_msg);
+        stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
         let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-  
+
   let perform_states query =
     if query = [] then [] else
     let is_tac e = match classify_vernac e with
@@ -1463,7 +1559,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
@@ -1520,9 +1616,9 @@ end = struct (* {{{ *)
           Future.from_val (Option.get (Global.body_of_constant_body c)) in
         let uc =
           Future.chain
-            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
-        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
-        let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+            ~pure:true uc Univ.hcons_universe_context_set in
+        let pr = Future.chain ~pure:true pr discharge in
+        let pr = Future.chain ~pure:true pr Constr.hcons in
         Future.sink pr;
         let extra = Future.join uc in
         u.(bucket) <- uc;
@@ -1603,7 +1699,7 @@ end = struct (* {{{ *)
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1687,7 +1783,7 @@ end = struct (* {{{ *)
         `Stay ((),[])
                     
   let on_marshal_error err { t_name } =
-    pr_err ("Fatal marshal error: " ^ t_name );
+    stm_pr_err ("Fatal marshal error: " ^ t_name );
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death = function
@@ -1715,7 +1811,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
@@ -1753,7 +1849,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 ->
@@ -1789,10 +1885,10 @@ end = struct (* {{{ *)
           let open Notations in
           try
             let pt, uc = Future.join f in
-            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+            stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
-              str"uc=" ++ Termops.pr_evar_universe_context uc)));
+              str"uc=" ++ Termops.pr_evar_universe_context uc));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
               Tactics.exact_no_check (EConstr.of_constr pt))
@@ -1834,7 +1930,7 @@ end = struct (* {{{ *)
   let use_response _ _ _ = `End
 
   let on_marshal_error _ _ =
-    pr_err ("Fatal marshal error in query");
+    stm_pr_err ("Fatal marshal error in query");
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death _ = ()
@@ -1846,11 +1942,11 @@ 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
-      let msg = pp_to_richpp (iprint e) in
+      let msg = iprint e     in
       feedback ~id:(State r_for) (Message (Error, None, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
@@ -1909,7 +2005,7 @@ let warn_deprecated_nested_proofs =
                     "stop working in a future Coq version"))
 
 let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
@@ -2009,7 +2105,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -2055,7 +2151,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
@@ -2096,16 +2192,16 @@ let known_state ?(redefine_qed=false) ~cache id =
     Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
-    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
     reach ~safe_id id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline (fun () -> "reached (cache)");
+      stm_prerr_endline (fun () -> "reached (cache)");
       State.install_cached id
     end else
     let step, cache_step, feedback_processed =
@@ -2134,24 +2230,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
@@ -2201,14 +2297,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;
@@ -2229,7 +2325,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));
@@ -2245,7 +2341,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;
@@ -2257,7 +2353,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       else cache_step in
     State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+    stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
@@ -2272,7 +2368,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline (fun () -> "Initializing workers");
+    stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -2324,9 +2420,9 @@ let rec join_admitted_proofs id =
 let join () =
   finish ();
   wait ();
-  prerr_endline (fun () -> "Joining the environment");
+  stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline (fun () -> "Joining Admitted proofs");
+  stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
@@ -2400,7 +2496,7 @@ let handle_failure (e, info) vcs tty =
       anomaly(str"error with no safe_id attached:" ++ spc() ++
         CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
-      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+      stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
       if tty && interactive () = `Yes then begin
         (* We stay on a valid state *)
@@ -2423,17 +2519,17 @@ let reset_task_queue = Slaves.reset_task_queue
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
   ({ verbose; loc; expr } as x) c =
-  prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
     let rc = begin
-      prerr_endline (fun () ->
+      stm_prerr_endline (fun () ->
         "  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
@@ -2467,7 +2563,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
+          stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2477,13 +2573,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
@@ -2556,7 +2652,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
@@ -2582,7 +2678,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
@@ -2612,12 +2708,12 @@ 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) }
       | _ -> ()
     end;
-    prerr_endline (fun () -> "processed }}}");
+    stm_prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
   with e ->
@@ -2803,7 +2899,7 @@ let edit_at id =
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
           CErrors.print_no_report e)
     | Some (_, id) ->
-        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+        stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         iraise (e, info)
@@ -2859,102 +2955,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..72b5380162 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,8 +4,8 @@ Vcs
 TQueue
 WorkerPool
 Vernac_classifier
-Lemmas
 CoqworkmgrApi
+WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index d5333d1077..256532c6b6 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
new file mode 100644
index 0000000000..50b42512cb
--- /dev/null
+++ b/stm/workerLoop.ml
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+let rec parse = function
+  | "--xml_format=Ppcmds" :: rest -> parse rest
+  | x :: rest -> x :: parse rest
+  | [] -> []
+
+let loop init args =
+  let args = parse args in
+  Flags.make_silent true;
+  init ();
+  CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+  args
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
new file mode 100644
index 0000000000..dcbf9c88d6
--- /dev/null
+++ b/stm/workerLoop.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+val loop : (unit -> unit) -> string list -> string list