[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 1179 insertions, 0 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
new file mode 100644
index 000000000..c1d9ae48a
--- /dev/null
+++ b/vernac/obligations.ml
@@ -0,0 +1,1179 @@
+open Printf
+open Globnames
+open Libobject
+open Entries
+open Decl_kinds
+open Declare
+
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+open Term
+open Vars
+open Names
+open Evd
+open Pp
+open CErrors
+open Util
+
+(* EJGA: This should go away, no more need for fix_exn  *)
+module Stm = struct
+    let u = (fun x -> x)
+    let get_fix_exn () = u
+end
+
+module NamedDecl = Context.Named.Declaration
+
+let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
+let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
+
+let succfix (depth, fixrels) =
+  (succ depth, List.map succ fixrels)
+
+let check_evars env evm =
+  Evar.Map.iter
+  (fun key evi ->
+   let (loc,k) = evar_source key evm in
+     match k with
+     | Evar_kinds.QuestionMark _
+     | Evar_kinds.ImplicitArg (_,_,false) -> ()
+     | _ ->
+       Pretype_errors.error_unsolvable_implicit ~loc env evm key None)
+  (Evd.undefined_map evm)
+
+type oblinfo =
+  { ev_name: int * Id.t;
+    ev_hyps: Context.Named.t;
+    ev_status: bool * Evar_kinds.obligation_definition_status;
+    ev_chop: int option;
+    ev_src: Evar_kinds.t Loc.located;
+    ev_typ: types;
+    ev_tac: unit Proofview.tactic option;
+    ev_deps: Int.Set.t }
+
+(** Substitute evar references in t using De Bruijn indices,
+  where n binders were passed through. *)
+
+let subst_evar_constr evs n idf t =
+  let seen = ref Int.Set.empty in
+  let transparent = ref Id.Set.empty in
+  let evar_info id = List.assoc_f Evar.equal id evs in
+  let rec substrec (depth, fixrels) c = match kind_of_term c with
+    | Evar (k, args) ->
+	let { ev_name = (id, idstr) ;
+	      ev_hyps = hyps ; ev_chop = chop } =
+	  try evar_info k
+	  with Not_found ->
+	    anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found")
+	in
+        seen := Int.Set.add id !seen;
+	  (* Evar arguments are created in inverse order,
+	     and we must not apply to defined ones (i.e. LetIn's)
+	  *)
+	let args =
+	  let n = match chop with None -> 0 | Some c -> c in
+	  let (l, r) = List.chop n (List.rev (Array.to_list args)) in
+	    List.rev r
+	in
+	let args =
+	  let rec aux hyps args acc =
+             let open Context.Named.Declaration in
+	     match hyps, args with
+		 (LocalAssum _ :: tlh), (c :: tla) ->
+		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
+	       | (LocalDef _ :: tlh), (_ :: tla) ->
+		   aux tlh tla acc
+	       | [], [] -> acc
+	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
+	  in aux hyps args []
+	in
+	  if List.exists
+            (fun x -> match kind_of_term x with
+            | Rel n -> Int.List.mem n fixrels
+            | _ -> false) args
+          then
+	    transparent := Id.Set.add idstr !transparent;
+	  mkApp (idf idstr, Array.of_list args)
+    | Fix _ ->
+	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
+    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
+  in
+  let t' = substrec (0, []) t in
+    t', !seen, !transparent
+
+
+(** Substitute variable references in t using De Bruijn indices,
+  where n binders were passed through. *)
+let subst_vars acc n t =
+  let var_index id = Util.List.index Id.equal id acc in
+  let rec substrec depth c = match kind_of_term c with
+    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in
+    substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+    Changes evars and hypothesis references to variable references.
+*)
+let etype_of_evar evs hyps concl =
+  let open Context.Named.Declaration in
+  let rec aux acc n = function
+      decl :: tl ->
+	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
+	let t'' = subst_vars acc 0 t' in
+	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
+	let s' = Int.Set.union s s' in
+	let trans' = Id.Set.union trans trans' in
+	  (match decl with
+            | LocalDef (id,c,_) ->
+		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
+		let c' = subst_vars acc 0 c' in
+		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
+		Int.Set.union s'' s',
+		Id.Set.union trans'' trans'
+	    | LocalAssum (id,_) ->
+		mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
+    | [] ->
+	let t', s, trans = subst_evar_constr evs n mkVar concl in
+	  subst_vars acc 0 t', s, trans
+  in aux [] 0 (List.rev hyps)
+
+let trunc_named_context n ctx =
+  let len = List.length ctx in
+    List.firstn (len - n) ctx
+
+let rec chop_product n t =
+  if Int.equal n 0 then Some t
+  else
+    match kind_of_term t with
+      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
+      | _ -> None
+
+let evar_dependencies evm oev =
+  let one_step deps =
+    Evar.Set.fold (fun ev s ->
+      let evi = Evd.find evm ev in
+      let deps' = evars_of_filtered_evar_info evi in
+      if Evar.Set.mem oev deps' then
+	invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
+      else Evar.Set.union deps' s)
+      deps deps
+  in
+  let rec aux deps =
+    let deps' = one_step deps in
+      if Evar.Set.equal deps deps' then deps
+      else aux deps'
+  in aux (Evar.Set.singleton oev)
+      
+let move_after (id, ev, deps as obl) l = 
+  let rec aux restdeps = function
+    | (id', _, _) as obl' :: tl -> 
+	let restdeps' = Evar.Set.remove id' restdeps in
+	  if Evar.Set.is_empty restdeps' then
+	    obl' :: obl :: tl
+	  else obl' :: aux restdeps' tl
+    | [] -> [obl]
+  in aux (Evar.Set.remove id deps) l
+    
+let sort_dependencies evl =
+  let rec aux l found list =
+    match l with
+    | (id, ev, deps) as obl :: tl ->
+	let found' = Evar.Set.union found (Evar.Set.singleton id) in
+	  if Evar.Set.subset deps found' then
+	    aux tl found' (obl :: list)
+	  else aux (move_after obl tl) found list
+    | [] -> List.rev list
+  in aux evl Evar.Set.empty []
+
+open Environ
+
+let eterm_obligations env name evm fs ?status t ty = 
+  (* 'Serialize' the evars *)
+  let nc = Environ.named_context env in
+  let nc_len = Context.Named.length nc in
+  let evm = Evarutil.nf_evar_map_undefined evm in
+  let evl = Evarutil.non_instantiated evm in
+  let evl = Evar.Map.bindings evl in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
+  let evn =
+    let i = ref (-1) in
+      List.rev_map (fun (id, ev) -> incr i;
+		      (id, (!i, Id.of_string
+			      (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
+		       ev)) evl
+  in
+  let evts =
+    (* Remove existential variables in types and build the corresponding products *)
+    List.fold_right
+      (fun (id, (n, nstr), ev) l ->
+	 let hyps = Evd.evar_filtered_context ev in
+	 let hyps = trunc_named_context nc_len hyps in
+	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
+	 let evtyp, hyps, chop =
+	   match chop_product fs evtyp with
+	   | Some t -> t, trunc_named_context fs hyps, fs
+	   | None -> evtyp, hyps, 0
+	 in
+	 let loc, k = evar_source id evm in
+	 let status = match k with
+           | Evar_kinds.QuestionMark o -> o
+           | _ -> match status with
+                 | Some o -> o
+                 | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
+         in
+         let force_status, status, chop = match status with
+	   | Evar_kinds.Define true as stat ->
+	      if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
+	      else false, stat, Some chop
+	   | s -> false, s, None
+	 in
+	 let info = { ev_name = (n, nstr);
+		      ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
+		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
+	 in (id, info) :: l)
+      evn []
+  in
+  let t', _, transparent = (* Substitute evar refs in the term by variables *)
+    subst_evar_constr evts 0 mkVar t 
+  in
+  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+  let evars = 
+    List.map (fun (ev, info) ->
+      let { ev_name = (_, name); ev_status = force_status, status;
+	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+      in
+      let force_status, status = match status with
+	| Evar_kinds.Define true when Id.Set.mem name transparent ->
+	  true, Evar_kinds.Define false
+	| _ -> force_status, status
+      in name, typ, src, (force_status, status), deps, tac) evts
+  in
+  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
+  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+    Array.of_list (List.rev evars), (evnames, evmap), t', ty
+
+let tactics_module = ["Program";"Tactics"]
+let safe_init_constant md name () =
+  Coqlib.check_required_library ("Coq"::md);
+  Coqlib.gen_constant "Obligations" md name
+let hide_obligation = safe_init_constant tactics_module "obligation"
+
+let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
+let error s = pperror (str s)
+
+let reduce c =
+  Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
+
+exception NoObligations of Id.t option
+
+let explain_no_obligations = function
+    Some ident -> str "No obligations for program " ++ Id.print ident
+  | None -> str "No obligations remaining"
+
+type obligation_info =
+    (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
+       (bool * Evar_kinds.obligation_definition_status)
+       * Int.Set.t * unit Proofview.tactic option) array
+
+type 'a obligation_body = 
+  | DefinedObl of 'a
+  | TermObl of constr
+
+type obligation =
+  { obl_name : Id.t;
+    obl_type : types;
+    obl_location : Evar_kinds.t Loc.located;
+    obl_body : constant obligation_body option;
+    obl_status : bool * Evar_kinds.obligation_definition_status;
+    obl_deps : Int.Set.t;
+    obl_tac : unit Proofview.tactic option;
+  }
+
+type obligations = (obligation array * int)
+
+type fixpoint_kind =
+  | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
+  | IsCoFixpoint
+
+type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+
+type program_info_aux = {
+  prg_name: Id.t;
+  prg_body: constr;
+  prg_type: constr;
+  prg_ctx:  Evd.evar_universe_context;
+  prg_pl: Id.t Loc.located list option;
+  prg_obligations: obligations;
+  prg_deps : Id.t list;
+  prg_fixkind : fixpoint_kind option ;
+  prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
+  prg_notations : notations ;
+  prg_kind : definition_kind;
+  prg_reduce : constr -> constr;
+  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
+  prg_opaque : bool;
+  prg_sign: named_context_val;
+}
+
+type program_info = program_info_aux CEphemeron.key
+
+let get_info x =
+  try CEphemeron.get x
+  with CEphemeron.InvalidKey ->
+    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+
+let assumption_message = Declare.assumption_message
+
+let default_tactic = ref (Proofview.tclUNIT ())
+
+(* true = hide obligations *)
+let hide_obligations = ref false
+
+let set_hide_obligations = (:=) hide_obligations
+let get_hide_obligations () = !hide_obligations
+
+open Goptions
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "Hidding of Program obligations";
+      optkey   = ["Hide";"Obligations"];
+      optread  = get_hide_obligations;
+      optwrite = set_hide_obligations; }
+
+let shrink_obligations = ref true
+
+let set_shrink_obligations = (:=) shrink_obligations
+let get_shrink_obligations () = !shrink_obligations
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true;
+      optname  = "Shrinking of Program obligations";
+      optkey   = ["Shrink";"Obligations"];
+      optread  = get_shrink_obligations;
+      optwrite = set_shrink_obligations; }
+
+let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
+
+let get_body obl =
+  match obl.obl_body with
+  | None -> None
+  | Some (DefinedObl c) ->
+    let ctx = Environ.constant_context (Global.env ()) c in
+    let pc = (c, Univ.UContext.instance ctx) in
+      Some (DefinedObl pc)
+  | Some (TermObl c) ->
+      Some (TermObl c)
+
+let get_obligation_body expand obl =
+  match get_body obl with
+  | None -> None
+  | Some c ->
+     if expand && snd obl.obl_status == Evar_kinds.Expand then
+       match c with
+       | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
+       | TermObl c -> Some c
+     else (match c with
+	   | DefinedObl pc -> Some (mkConstU pc)
+	   | TermObl c -> Some c)
+
+let obl_substitution expand obls deps =
+  Int.Set.fold
+    (fun x acc ->
+       let xobl = obls.(x) in
+       match get_obligation_body expand xobl with
+       | None -> acc
+       | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
+    deps []
+
+let subst_deps expand obls deps t =
+  let osubst = obl_substitution expand obls deps in
+    (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
+
+let rec prod_app t n =
+  match kind_of_term (Termops.strip_outer_cast t) with
+    | Prod (_,_,b) -> subst1 n b
+    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
+    | _ ->
+	user_err ~hdr:"prod_app"
+	  (str"Needed a product, but didn't find one" ++ fnl ())
+
+
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
+
+let replace_appvars subst =
+  let rec aux c = 
+    let f, l = decompose_app c in
+      if isVar f then
+	try
+	  let c' = List.map (map_constr aux) l in
+	  let (t, b) = Id.List.assoc (destVar f) subst in
+	    mkApp (delayed_force hide_obligation, 
+		   [| prod_applist t c'; applistc b c' |])
+	with Not_found -> map_constr aux c
+      else map_constr aux c
+  in map_constr aux
+       
+let subst_prog expand obls ints prg =
+  let subst = obl_substitution expand obls ints in
+    if get_hide_obligations () then
+      (replace_appvars subst prg.prg_body,
+       replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
+    else 
+      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
+	(Vars.replace_vars subst' prg.prg_body,
+	 Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
+
+let subst_deps_obl obls obl =
+  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
+    { obl with obl_type = t' }
+
+module ProgMap = Id.Map
+
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
+
+let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
+
+let from_prg : program_info ProgMap.t ref =
+  Summary.ref ProgMap.empty ~name:"program-tcc-table"
+
+let close sec =
+  if not (ProgMap.is_empty !from_prg) then
+    let keys = map_keys !from_prg in
+      user_err ~hdr:"Program" 
+	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
+	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
+	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
+	      str "unsolved obligations"))
+
+let input : program_info ProgMap.t -> obj =
+  declare_object
+    { (default_object "Program state") with
+      cache_function = (fun (na, pi) -> from_prg := pi);
+      load_function = (fun _ (_, pi) -> from_prg := pi);
+      discharge_function = (fun _ -> close "section"; None);
+      classify_function = (fun _ -> close "module"; Dispose) }
+    
+open Evd
+
+let progmap_remove prg =
+  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
+  
+let progmap_add n prg =
+  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
+
+let progmap_replace prg' = 
+  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
+
+let rec intset_to = function
+    -1 -> Int.Set.empty
+  | n -> Int.Set.add n (intset_to (pred n))
+
+let subst_body expand prg =
+  let obls, _ = prg.prg_obligations in
+  let ints = intset_to (pred (Array.length obls)) in
+    subst_prog expand obls ints prg
+
+let declare_definition prg =
+  let body, typ = subst_body true prg in
+  let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+    (Evd.evar_universe_context_subst prg.prg_ctx) in
+  let opaque = prg.prg_opaque in
+  let fix_exn = Stm.get_fix_exn () in
+  let pl, ctx =
+    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
+  let ce =
+    definition_entry ~fix_exn
+     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+  in
+  let () = progmap_remove prg in
+  let cst =
+    !declare_definition_ref prg.prg_name 
+     prg.prg_kind ce prg.prg_implicits
+     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+  in
+  Universes.register_universe_binders cst pl;
+  cst
+      
+open Pp
+
+let rec lam_index n t acc =
+  match kind_of_term t with
+    | Lambda (Name n', _, _) when Id.equal n n' ->
+      acc
+    | Lambda (_, _, b) ->
+	lam_index n b (succ acc)
+    | _ -> raise Not_found
+
+let compute_possible_guardness_evidences (n,_) fixbody fixtype =
+  match n with
+  | Some (loc, n) -> [lam_index n fixbody 0]
+  | None ->
+      (* If recursive argument was not given by user, we try all args.
+	 An earlier approach was to look only for inductive arguments,
+	 but doing it properly involves delta-reduction, and it finally
+         doesn't seem to worth the effort (except for huge mutual
+	 fixpoints ?) *)
+      let m = Termops.nb_prod fixtype in
+      let ctx = fst (decompose_prod_n_assum m fixtype) in
+	List.map_i (fun i _ -> i) 0 ctx
+
+let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
+
+let declare_mutual_definition l =
+  let len = List.length l in
+  let first = List.hd l in
+  let fixdefs, fixtypes, fiximps =
+    List.split3
+      (List.map (fun x -> 
+	let subs, typ = (subst_body true x) in
+	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
+	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
+	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
+  in
+(*   let fixdefs = List.map reduce_fix fixdefs in *)
+  let fixkind = Option.get first.prg_fixkind in
+  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
+  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+  let (local,poly,kind) = first.prg_kind in
+  let fixnames = first.prg_deps in
+  let opaque = first.prg_opaque in
+  let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
+  let indexes, fixdecls =
+    match fixkind with
+      | IsFixpoint wfl ->
+	  let possible_indexes =
+	    List.map3 compute_possible_guardness_evidences
+              wfl fixdefs fixtypes in
+	  let indexes = 
+              Pretyping.search_guard
+              Loc.ghost (Global.env())
+              possible_indexes fixdecls in
+          Some indexes, 
+          List.map_i (fun i _ ->
+            mk_proof (mkFix ((indexes,i),fixdecls))) 0 l
+      | IsCoFixpoint ->
+          None,
+          List.map_i (fun i _ ->
+            mk_proof (mkCoFix (i,fixdecls))) 0 l
+  in
+  (* Declare the recursive definitions *)
+  let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let fix_exn = Stm.get_fix_exn () in
+  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
+    fixnames fixdecls fixtypes fiximps in
+    (* Declare notations *)
+    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
+    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+    let gr = List.hd kns in
+    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    List.iter progmap_remove l; kn
+
+let decompose_lam_prod c ty =
+  let open Context.Rel.Declaration in
+  let rec aux ctx c ty =
+    match kind_of_term c, kind_of_term ty with
+    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
+	 when eq_constr b b' && eq_constr t t' ->
+       let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
+       aux ctx' c ty
+    | _, LetIn (x', b', t', ty) ->
+       let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in
+       aux ctx' (lift 1 c) ty
+    | LetIn (x, b, t, c), _ ->
+       let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in
+       aux ctx' c (lift 1 ty)
+    | Lambda (x, b, t), Prod (x', b', t')
+       (* By invariant, must be convertible *) ->
+       let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in
+       aux ctx' t t'
+    | Cast (c, _, _), _ -> aux ctx c ty
+    | _, _ -> ctx, c, ty
+  in aux Context.Rel.empty c ty
+
+let shrink_body c ty =
+  let ctx, b, ty =
+    match ty with
+    | None ->
+       let ctx, b = decompose_lam_assum c in
+       ctx, b, None
+    | Some ty ->
+       let ctx, b, ty = decompose_lam_prod c ty in
+       ctx, b, Some ty
+  in
+  let b', ty', n, args =
+    List.fold_left (fun (b, ty, i, args) decl ->
+        if noccurn 1 b && Option.cata (noccurn 1) true ty then
+	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
+	else
+          let open Context.Rel.Declaration in
+	  let args = if is_local_assum decl then mkRel i :: args else args in
+          mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
+	  succ i, args)
+     (b, ty, 1, []) ctx
+  in ctx, b', ty', Array.of_list args
+
+let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+
+let add_hint local prg cst =
+  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+
+let declare_obligation prg obl body ty uctx =
+  let body = prg.prg_reduce body in
+  let ty = Option.map prg.prg_reduce ty in
+  match obl.obl_status with
+  | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
+  | force, Evar_kinds.Define opaque ->
+      let opaque = not force && opaque in
+      let poly = pi2 prg.prg_kind in
+      let ctx, body, ty, args =
+	if get_shrink_obligations () && not poly then
+	  shrink_body body ty else [], body, ty, [||]
+      in
+      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+      let ce =
+        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
+          const_entry_secctx = None;
+	  const_entry_type = ty;
+	  const_entry_polymorphic = poly;
+	  const_entry_universes = uctx;
+	  const_entry_opaque = opaque;
+          const_entry_inline_code = false;
+          const_entry_feedback = None;
+      } in
+      (** ppedrot: seems legit to have obligations as local *)
+      let constant = Declare.declare_constant obl.obl_name ~local:true
+	(DefinitionEntry ce,IsProof Property)
+      in
+	if not opaque then add_hint false prg constant;
+	definition_message obl.obl_name;
+	true, { obl with obl_body =
+	    if poly then
+	      Some (DefinedObl constant)
+	    else
+	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
+
+let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+		   notations obls impls kind reduce hook =
+  let obls', b =
+    match b with
+    | None ->
+	assert(Int.equal (Array.length obls) 0);
+	let n = Nameops.add_suffix n "_obligation" in
+	  [| { obl_name = n; obl_body = None;
+	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
+	       obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
+	       obl_tac = None } |],
+	mkVar n
+    | Some b ->
+	Array.mapi
+	  (fun i (n, t, l, o, d, tac) ->
+            { obl_name = n ; obl_body = None; 
+	      obl_location = l; obl_type = t; obl_status = o;
+	      obl_deps = d; obl_tac = tac })
+	  obls, b
+  in
+    { prg_name = n ; prg_body = b; prg_type = reduce t; 
+      prg_ctx = ctx; prg_pl = pl;
+      prg_obligations = (obls', Array.length obls');
+      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
+      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
+      prg_hook = hook; prg_opaque = opaque;
+      prg_sign = sign }
+
+let map_cardinal m =
+  let i = ref 0 in
+  ProgMap.iter (fun _ v ->
+		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
+  !i
+
+exception Found of program_info
+
+let map_first m =
+  try
+    ProgMap.iter (fun _ v ->
+		  if snd (CEphemeron.get v).prg_obligations > 0 then
+		    raise (Found v)) m;
+    assert(false)
+  with Found x -> x
+
+let get_prog name =
+  let prg_infos = !from_prg in
+    match name with
+	Some n ->
+	  (try get_info (ProgMap.find n prg_infos)
+	   with Not_found -> raise (NoObligations (Some n)))
+      | None ->
+	  (let n = map_cardinal prg_infos in
+	     match n with
+		 0 -> raise (NoObligations None)
+	       | 1 -> get_info (map_first prg_infos)
+	       | _ ->
+                let progs = Id.Set.elements (ProgMap.domain prg_infos) in
+                let prog = List.hd progs in
+                let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
+                user_err 
+                  (str "More than one program with unsolved obligations: " ++ progs
+                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
+
+let get_any_prog () =
+  let prg_infos = !from_prg in
+  let n = map_cardinal prg_infos in
+  if n > 0 then get_info (map_first prg_infos)
+  else raise (NoObligations None)
+
+let get_prog_err n =
+  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
+
+let get_any_prog_err () =
+  try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)
+
+let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
+
+let all_programs () =
+  ProgMap.fold (fun k p l -> p :: l) !from_prg []
+
+type progress =
+    | Remain of int
+    | Dependent
+    | Defined of global_reference
+
+let obligations_message rem =
+  if rem > 0 then
+    if Int.equal rem 1 then
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
+    else
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
+  else
+    Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
+
+let update_obls prg obls rem =
+  let prg' = { prg with prg_obligations = (obls, rem) } in
+    progmap_replace prg';
+    obligations_message rem;
+    if rem > 0 then Remain rem
+    else (
+      match prg'.prg_deps with
+      | [] ->
+	  let kn = declare_definition prg' in
+	    progmap_remove prg';
+	    Defined kn
+      | l ->
+	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
+	    if List.for_all (fun x -> obligations_solved x) progs then
+	      let kn = declare_mutual_definition progs in
+		Defined (ConstRef kn)
+	    else Dependent)
+
+let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
+
+let deps_remaining obls deps =
+  Int.Set.fold
+    (fun x acc ->
+      if is_defined obls x then acc
+      else x :: acc)
+    deps []
+
+let dependencies obls n =
+  let res = ref Int.Set.empty in
+    Array.iteri
+      (fun i obl ->
+	if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then
+	  res := Int.Set.add i !res)
+      obls;
+    !res
+
+let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
+
+let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
+
+let kind_of_obligation poly o =
+  match o with
+  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
+  | _ -> goal_proof_kind poly
+
+let not_transp_msg =
+  str "Obligation should be transparent but was declared opaque." ++ spc () ++
+    str"Use 'Defined' instead."
+
+let err_not_transp () = pperror not_transp_msg
+
+let rec string_of_list sep f = function
+    [] -> ""
+  | x :: [] -> f x
+  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+
+let solve_by_tac name evi t poly ctx =
+  let id = name in
+  let concl = evi.evar_concl in
+  (* spiwack: the status is dropped. *)
+  let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
+    id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
+  let env = Global.env () in
+  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+  let body, eff = Future.force entry.const_entry_body in
+  assert(Safe_typing.empty_private_constants = eff);
+  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
+  Inductiveops.control_only_guard (Global.env ()) (fst body);
+  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
+
+let obligation_terminator name num guard hook auto pf =
+  let open Proof_global in
+  let term = Lemmas.universe_proof_terminator guard hook in
+  match pf with
+  | Admitted _ -> apply_terminator term pf
+  | Proved (opq, id, proof) ->
+    if not !shrink_obligations then apply_terminator term pf
+    else
+      let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+      let env = Global.env () in
+      let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+      let ty = entry.Entries.const_entry_type in
+      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
+      assert(Safe_typing.empty_private_constants = eff);
+      let sigma = Evd.from_ctx (fst uctx) in
+      let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
+      Inductiveops.control_only_guard (Global.env ()) body;
+      (** Declare the obligation ourselves and drop the hook *)
+      let prg = get_info (ProgMap.find name !from_prg) in
+      let ctx = Evd.evar_universe_context sigma in
+      let prg = { prg with prg_ctx = ctx } in
+      let obls, rem = prg.prg_obligations in
+      let obl = obls.(num) in
+      let status =
+        match obl.obl_status, opq with
+        | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
+        | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
+        | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+        | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
+        | (_, status), Vernacexpr.Transparent -> status
+      in
+      let obl = { obl with obl_status = false, status } in
+      let uctx = Evd.evar_context_universe_context ctx in
+      let (_, obl) = declare_obligation prg obl body ty uctx in
+      let obls = Array.copy obls in
+      let _ = obls.(num) <- obl in
+      try
+      ignore (update_obls prg obls (pred rem));
+      if pred rem > 0 then
+        begin
+	  let deps = dependencies obls num in
+	  if not (Int.Set.is_empty deps) then
+	    ignore (auto (Some name) None deps)
+	end
+      with e when CErrors.noncritical e ->
+        let e = CErrors.push e in
+        pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+
+let obligation_hook prg obl num auto ctx' _ gr =
+  let obls, rem = prg.prg_obligations in
+  let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+  let transparent = evaluable_constant cst (Global.env ()) in
+  let () = match obl.obl_status with
+      (true, Evar_kinds.Expand) 
+    | (true, Evar_kinds.Define true) ->
+       if not transparent then err_not_transp ()
+    | _ -> ()
+in
+  let obl = { obl with obl_body = Some (DefinedObl cst) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
+  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
+  let ctx' =
+    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      let evd = Evd.from_env (Global.env ()) in
+      let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
+        Evd.evar_universe_context ctx'
+    else ctx'
+  in
+  let prg = { prg with prg_ctx = ctx' } in
+  let () =
+    try ignore (update_obls prg obls (pred rem))
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+  in
+  if pred rem > 0 then begin
+    let deps = dependencies obls num in
+    if not (Int.Set.is_empty deps) then
+      ignore (auto (Some prg.prg_name) None deps)
+  end
+
+let rec solve_obligation prg num tac =
+  let user_num = succ num in
+  let obls, rem = prg.prg_obligations in
+  let obl = obls.(num) in
+  let remaining = deps_remaining obls obl.obl_deps in
+  let () =
+    if not (Option.is_empty obl.obl_body) then
+      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
+    if not (List.is_empty remaining) then
+      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
+  in
+  let obl = subst_deps_obl obls obl in
+  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
+  let evd = Evd.from_ctx prg.prg_ctx in
+  let evd = Evd.update_sigma_env evd (Global.env ()) in
+  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
+  let terminator guard hook =
+    Proof_global.make_terminator
+      (obligation_terminator prg.prg_name num guard hook auto) in
+  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
+  let _ = Pfedit.by !default_tactic in
+  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
+
+and obligation (user_num, name, typ) tac =
+  let num = pred user_num in
+  let prg = get_prog_err name in
+  let obls, rem = prg.prg_obligations in
+    if num < Array.length obls then
+      let obl = obls.(num) in
+	match obl.obl_body with
+	    None -> solve_obligation prg num tac
+	  | Some r -> error "Obligation already solved"
+    else error (sprintf "Unknown obligation number %i" (succ num))
+
+
+and solve_obligation_by_tac prg obls i tac =
+  let obl = obls.(i) in
+    match obl.obl_body with
+    | Some _ -> None
+    | None ->
+	try
+	  if List.is_empty (deps_remaining obls obl.obl_deps) then
+	    let obl = subst_deps_obl obls obl in
+	    let tac =
+	      match tac with
+	      | Some t -> t
+	      | None ->
+		  match obl.obl_tac with
+		  | Some t -> t
+		  | None -> !default_tactic
+	    in
+	    let evd = Evd.from_ctx prg.prg_ctx in
+	    let evd = Evd.update_sigma_env evd (Global.env ()) in
+	    let t, ty, ctx =
+	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+	    in
+	    let uctx = Evd.evar_context_universe_context ctx in
+	    let prg = {prg with prg_ctx = ctx} in
+	    let def, obl' = declare_obligation prg obl t ty uctx in
+	      obls.(i) <- obl';
+	      if def && not (pi2 prg.prg_kind) then (
+	        (* Declare the term constraints with the first obligation only *)
+	        let evd = Evd.from_env (Global.env ()) in
+	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
+		let ctx' = Evd.evar_universe_context evd in
+		  Some {prg with prg_ctx = ctx'})
+	      else Some prg
+	  else None
+	with e when CErrors.noncritical e ->
+          let (e, _) = CErrors.push e in
+          match e with
+	  | Refiner.FailError (_, s) ->
+	      user_err ~loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s)
+          | e -> None (* FIXME really ? *)
+
+and solve_prg_obligations prg ?oblset tac =
+  let obls, rem = prg.prg_obligations in
+  let rem = ref rem in
+  let obls' = Array.copy obls in
+  let set = ref Int.Set.empty in
+  let p = match oblset with
+    | None -> (fun _ -> true)
+    | Some s -> set := s;
+      (fun i -> Int.Set.mem i !set)
+  in
+  let prgref = ref prg in
+  let _ =
+    Array.iteri (fun i x ->
+      if p i then
+        match solve_obligation_by_tac !prgref obls' i tac with
+	| None -> ()
+ 	| Some prg' ->
+	   prgref := prg';
+	   let deps = dependencies obls i in
+ 	   (set := Int.Set.union !set deps;
+ 	    decr rem))
+      obls'
+  in
+    update_obls !prgref obls' !rem
+
+and solve_obligations n tac =
+  let prg = get_prog_err n in
+    solve_prg_obligations prg tac
+
+and solve_all_obligations tac =
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
+
+and try_solve_obligation n prg tac =
+  let prg = get_prog prg in
+  let obls, rem = prg.prg_obligations in
+  let obls' = Array.copy obls in
+    match solve_obligation_by_tac prg obls' n tac with
+    | Some prg' -> ignore(update_obls prg' obls' (pred rem))
+    | None -> ()
+
+and try_solve_obligations n tac =
+  try ignore (solve_obligations n tac) with NoObligations _ -> ()
+
+and auto_solve_obligations n ?oblset tac : progress =
+  Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
+  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
+
+open Pp
+let show_obligations_of_prg ?(msg=true) prg =
+  let n = prg.prg_name in
+  let obls, rem = prg.prg_obligations in
+  let showed = ref 5 in
+    if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
+    Array.iteri (fun i x ->
+		   match x.obl_body with
+		   | None ->
+		       if !showed > 0 then (
+		         decr showed;
+			 let x = subst_deps_obl obls x in
+			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
+				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
+					    str "." ++ fnl ())))
+		   | Some _ -> ())
+      obls
+
+let show_obligations ?(msg=true) n =
+  let progs = match n with
+    | None -> all_programs ()
+    | Some n ->
+	try [ProgMap.find n !from_prg]
+	with Not_found -> raise (NoObligations (Some n))
+  in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
+
+let show_term n =
+  let prg = get_prog_err n in
+  let n = prg.prg_name in
+    (Id.print n ++ spc () ++ str":" ++ spc () ++
+	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
+
+let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+  let sign = Decls.initialize_named_context_for_proof () in
+  let info = Id.print n ++ str " has type-checked" in
+  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
+  let obls,_ = prg.prg_obligations in
+  if Int.equal (Array.length obls) 0 then (
+    Flags.if_verbose Feedback.msg_info (info ++ str ".");
+    let cst = declare_definition prg in
+      Defined cst)
+  else (
+    let len = Array.length obls in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+      progmap_add n (CEphemeron.create prg);
+      let res = auto_solve_obligations (Some n) tactic in
+	match res with
+	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+	| _ -> res)
+
+let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+  let sign = Decls.initialize_named_context_for_proof () in
+  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
+    List.iter
+    (fun  (n, b, t, imps, obls) ->
+     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
+       notations obls imps kind reduce hook 
+     in progmap_add n (CEphemeron.create prg)) l;
+    let _defined =
+      List.fold_left (fun finished x ->
+	if finished then finished
+	else
+	  let res = auto_solve_obligations (Some x) tactic in
+	    match res with
+	    | Defined _ -> 
+		(* If one definition is turned into a constant, 
+		   the whole block is defined. *) true
+	    | _ -> false)
+	false deps
+    in ()
+
+let admit_prog prg =
+  let obls, rem = prg.prg_obligations in
+  let obls = Array.copy obls in
+    Array.iteri 
+      (fun i x ->
+        match x.obl_body with
+        | None ->
+            let x = subst_deps_obl obls x in
+	    let ctx = Evd.evar_context_universe_context prg.prg_ctx in
+            let kn = Declare.declare_constant x.obl_name ~local:true
+              (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
+            in
+              assumption_message x.obl_name;
+              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
+        | Some _ -> ())
+      obls;
+    ignore(update_obls prg obls 0)
+
+let rec admit_all_obligations () =
+  let prg = try Some (get_any_prog ()) with NoObligations _ -> None in
+  match prg with
+  | None -> ()
+  | Some prg ->
+    admit_prog prg;
+    admit_all_obligations ()
+
+let admit_obligations n =
+  match n with
+  | None -> admit_all_obligations ()
+  | Some _ ->
+    let prg = get_prog_err n in
+    admit_prog prg
+
+let next_obligation n tac =
+  let prg = match n with
+  | None -> get_any_prog_err ()
+  | Some _ -> get_prog_err n
+  in
+  let obls, rem = prg.prg_obligations in
+  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
+  let i = match Array.findi is_open obls with
+  | Some i -> i
+  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
+  in
+  solve_obligation prg i tac
+
+let init_program () =
+  Coqlib.check_required_library Coqlib.datatypes_module_name;
+  Coqlib.check_required_library ["Coq";"Init";"Specif"];
+  Coqlib.check_required_library ["Coq";"Program";"Tactics"]
+
+
+let set_program_mode c =
+  if c then
+    if !Flags.program_mode then ()
+    else begin
+      init_program ();
+      Flags.program_mode := true;
+    end