[obligations] More progress towards unification of the save path

We make internal types `private` as an step towards the unification of
the save path with the rest of the system.

In particular, this is allow us to guarantee invariants
w.r.t. external users as the large majority of fields are always
constant.

This will also enable at some point a common creation of proof entry
with the rest of the system.

4 files changed, 242 insertions, 180 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 73356c42f1..62556d38ff 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
     Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+    DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
 
   type partial_state =
     [ `Full of Vernacstate.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 8b0666aab7..df39f7be4b 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -18,39 +18,94 @@ open Entries
 
 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 : pconstant obligation_body option
-  ; obl_status : bool * Evar_kinds.obligation_definition_status
-  ; obl_deps : Int.Set.t
-  ; obl_tac : unit Proofview.tactic option }
+module Obligation = struct
+  type t =
+    { obl_name : Id.t
+    ; obl_type : types
+    ; obl_location : Evar_kinds.t Loc.located
+    ; obl_body : pconstant 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
+  let set_type ~typ obl = { obl with obl_type = typ }
+  let set_body ~body obl = { obl with obl_body = Some body }
+
+end
+
+type obligations = Obligation.t array * int
 
 type fixpoint_kind =
   | IsFixpoint of lident option list
   | IsCoFixpoint
 
-type program_info =
-  { prg_name : Id.t
-  ; prg_body : constr
-  ; prg_type : constr
-  ; prg_ctx : UState.t
-  ; prg_univdecl : UState.universe_decl
-  ; prg_obligations : obligations
-  ; prg_deps : Id.t list
-  ; prg_fixkind : fixpoint_kind option
-  ; prg_implicits : Impargs.manual_implicits
-  ; prg_notations : Vernacexpr.decl_notation list
-  ; prg_poly : bool
-  ; prg_scope : DeclareDef.locality
-  ; prg_kind : Decls.definition_object_kind
-  ; prg_reduce : constr -> constr
-  ; prg_hook : DeclareDef.Hook.t option
-  ; prg_opaque : bool
-  }
+module ProgramDecl = struct
+
+  type t =
+    { prg_name : Id.t
+    ; prg_body : constr
+    ; prg_type : constr
+    ; prg_ctx : UState.t
+    ; prg_univdecl : UState.universe_decl
+    ; prg_obligations : obligations
+    ; prg_deps : Id.t list
+    ; prg_fixkind : fixpoint_kind option
+    ; prg_implicits : Impargs.manual_implicits
+    ; prg_notations : Vernacexpr.decl_notation list
+    ; prg_poly : bool
+    ; prg_scope : DeclareDef.locality
+    ; prg_kind : Decls.definition_object_kind
+    ; prg_reduce : constr -> constr
+    ; prg_hook : DeclareDef.Hook.t option
+    ; prg_opaque : bool
+    }
+
+  open Obligation
+
+  let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs
+      ~poly ~scope ~kind b t deps fixkind notations obls reduce =
+    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.tag 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
+    let ctx = UState.make_flexible_nonalgebraic uctx in
+    { prg_name = n
+    ; prg_body = b
+    ; prg_type = reduce t
+    ; prg_ctx = ctx
+    ; prg_univdecl = udecl
+    ; prg_obligations = (obls', Array.length obls')
+    ; prg_deps = deps
+    ; prg_fixkind = fixkind
+    ; prg_notations = notations
+    ; prg_implicits = impargs
+    ; prg_poly = poly
+    ; prg_scope = scope
+    ; prg_kind = kind
+    ; prg_reduce = reduce
+    ; prg_hook = hook
+    ; prg_opaque = opaque
+    }
+
+  let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
+end
+
+open Obligation
+open ProgramDecl
 
 (* Saving an obligation *)
 
@@ -120,16 +175,16 @@ let shrink_body c ty =
   in
   (ctx, b', ty', Array.of_list args)
 
+(***********************************************************************)
+(* Saving an obligation                                                *)
+(***********************************************************************)
+
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
   let locality = if local then Goptions.OptLocal else Goptions.OptExport in
   Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
 
-(***********************************************************************)
-(* Saving an obligation                                                *)
-(***********************************************************************)
-
 (* true = hide obligations *)
 let get_hide_obligations =
   Goptions.declare_bool_option_and_ref
@@ -205,7 +260,7 @@ let close sec =
         ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ")
            ++ str "unsolved obligations" ))
 
-let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj =
+let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj =
   let open Libobject in
   declare_object
     { (default_object "Program state") with
@@ -543,3 +598,39 @@ let obligation_terminator entries uctx { name; num; auto } =
         str
           "[obligation_terminator] close_proof returned more than one proof \
            term")
+
+(* Similar to the terminator but for interactive paths, as the
+   terminator is only called in interactive proof mode *)
+let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
+  let obls, rem = prg.prg_obligations in
+  let cst = match dref with GlobRef.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 inst, ctx' =
+    if not prg.prg_poly (* Not polymorphic *) then
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
+      Univ.Instance.empty, ctx'
+    else
+      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+      let uctx = UState.context ctx' in
+      Univ.UContext.instance uctx, ctx'
+  in
+  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let () = obls.(num) <- obl in
+  let prg = { prg with prg_ctx = ctx' } in
+  let () = ignore (update_obls prg obls (pred rem)) 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) deps None)
+  end
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 6e7700a28a..c2bd0595fa 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -13,61 +13,99 @@ open Constr
 
 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 : pconstant obligation_body option
-  ; obl_status : bool * Evar_kinds.obligation_definition_status
-  ; obl_deps : Int.Set.t
-  ; obl_tac : unit Proofview.tactic option }
+module Obligation : sig
 
-type obligations = obligation array * int
+  type t = private
+    { obl_name : Id.t
+    ; obl_type : types
+    ; obl_location : Evar_kinds.t Loc.located
+    ; obl_body : pconstant obligation_body option
+    ; obl_status : bool * Evar_kinds.obligation_definition_status
+    ; obl_deps : Int.Set.t
+    ; obl_tac : unit Proofview.tactic option }
+
+  val set_type : typ:Constr.types -> t -> t
+  val set_body : body:pconstant obligation_body -> t -> t
+
+end
+
+type obligations = Obligation.t array * int
 
 type fixpoint_kind =
   | IsFixpoint of lident option list
   | IsCoFixpoint
 
-type program_info =
-  { prg_name : Id.t
-  ; prg_body : constr
-  ; prg_type : constr
-  ; prg_ctx : UState.t
-  ; prg_univdecl : UState.universe_decl
-  ; prg_obligations : obligations
-  ; prg_deps : Id.t list
-  ; prg_fixkind : fixpoint_kind option
-  ; prg_implicits : Impargs.manual_implicits
-  ; prg_notations : Vernacexpr.decl_notation list
-  ; prg_poly : bool
-  ; prg_scope : DeclareDef.locality
-  ; prg_kind : Decls.definition_object_kind
-  ; prg_reduce : constr -> constr
-  ; prg_hook : DeclareDef.Hook.t option
-  ; prg_opaque : bool
-  }
+(* Information about a single [Program {Definition,Lemma,..}] declaration *)
+module ProgramDecl : sig
+
+  type t = private
+    { prg_name : Id.t
+    ; prg_body : constr
+    ; prg_type : constr
+    ; prg_ctx : UState.t
+    ; prg_univdecl : UState.universe_decl
+    ; prg_obligations : obligations
+    ; prg_deps : Id.t list
+    ; prg_fixkind : fixpoint_kind option
+    ; prg_implicits : Impargs.manual_implicits
+    ; prg_notations : Vernacexpr.decl_notation list
+    ; prg_poly : bool
+    ; prg_scope : DeclareDef.locality
+    ; prg_kind : Decls.definition_object_kind
+    ; prg_reduce : constr -> constr
+    ; prg_hook : DeclareDef.Hook.t option
+    ; prg_opaque : bool
+    }
+
+  val make :
+    ?opaque:bool
+    -> ?hook:DeclareDef.Hook.t
+    -> Names.Id.t
+    -> udecl:UState.universe_decl
+    -> uctx:UState.t
+    -> impargs:Impargs.manual_implicits
+    -> poly:bool
+    -> scope:DeclareDef.locality
+    -> kind:Decls.definition_object_kind
+    -> Constr.constr option
+    -> Constr.types
+    -> Names.Id.t list
+    -> fixpoint_kind option
+    -> Vernacexpr.decl_notation list
+    -> ( Names.Id.t
+         * Constr.types
+         * Evar_kinds.t Loc.located
+         * (bool * Evar_kinds.obligation_definition_status)
+         * Int.Set.t
+         * unit Proofview.tactic option )
+      array
+    -> (Constr.constr -> Constr.constr)
+    -> t
+
+  val set_uctx : uctx:UState.t -> t -> t
+end
 
 val declare_obligation :
-     program_info
-  -> obligation
+     ProgramDecl.t
+  -> Obligation.t
   -> Constr.types
   -> Constr.types option
   -> Entries.universes_entry
-  -> bool * obligation
+  -> bool * Obligation.t
 (** [declare_obligation] Save an obligation *)
 
 module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
 
-val declare_definition : program_info -> Names.GlobRef.t
+val declare_definition : ProgramDecl.t -> Names.GlobRef.t
 
+(** Resolution status of a program *)
 type progress =
-  (* Resolution status of a program *)
   | Remain of int
-  (* n obligations remaining *)
+  (** n obligations remaining *)
   | Dependent
-  (* Dependent on other definitions *)
+  (** Dependent on other definitions *)
   | Defined of GlobRef.t
-  (* Defined as id *)
+  (** Defined as id *)
 
 type obligation_qed_info =
   { name : Id.t
@@ -79,32 +117,41 @@ val obligation_terminator
   : Evd.side_effects Declare.proof_entry list
   -> UState.t
   -> obligation_qed_info -> unit
-(** [obligation_terminator] part 2 of saving an obligation *)
+(** [obligation_terminator] part 2 of saving an obligation, proof mode *)
+
+val obligation_hook
+  : ProgramDecl.t
+  -> Obligation.t
+  -> Int.t
+  -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b)
+  -> DeclareDef.Hook.S.t
+  -> unit
+(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *)
 
 val update_obls :
-     program_info
-  -> obligation array
+     ProgramDecl.t
+  -> Obligation.t array
   -> int
   -> progress
 (** [update_obls prg obls n progress] What does this do? *)
 
 (** { 2 Util }  *)
 
-val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t
+val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t
 
 val program_tcc_summary_tag :
-  program_info CEphemeron.key Id.Map.t Summary.Dyn.tag
+  ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag
 
 val obl_substitution :
      bool
-  -> obligation array
+  -> Obligation.t array
   -> Int.Set.t
   -> (ProgMap.key * (Constr.types * Constr.types)) list
 
-val dependencies : obligation array -> int -> Int.Set.t
+val dependencies : Obligation.t array -> int -> Int.Set.t
 
 val err_not_transp : unit -> unit
-val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit
+val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9418231cf5..a9d43e851d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -28,7 +28,10 @@ open Util
 
 module NamedDecl = Context.Named.Declaration
 
+(* For the records fields, opens should go away one these types are private *)
 open DeclareObl
+open DeclareObl.Obligation
+open DeclareObl.ProgramDecl
 
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
@@ -189,8 +192,6 @@ let sort_dependencies evl =
     | [] -> 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
@@ -284,66 +285,22 @@ let default_tactic = ref (Proofview.tclUNIT ())
 let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
 
 let subst_deps expand obls deps t =
-  let osubst = obl_substitution expand obls deps in
+  let osubst = DeclareObl.obl_substitution expand obls deps in
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
 let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
-    { obl with obl_type = t' }
+  Obligation.set_type ~typ:t' obl
 
 open Evd
 
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
-
-let add_local_hint prg cst =
-  Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst)
-
-let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
-                   notations obls impls ~scope ~poly ~kind reduce =
-  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.tag 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
-  let ctx = UState.make_flexible_nonalgebraic ctx in
-    { prg_name = n
-    ; prg_body = b
-    ; prg_type = reduce t
-    ; prg_ctx = ctx
-    ; prg_univdecl = udecl
-    ; prg_obligations = (obls', Array.length obls')
-    ; prg_deps = deps
-    ; prg_fixkind = fixkind
-    ; prg_notations = notations
-    ; prg_implicits = impls
-    ; prg_poly = poly
-    ; prg_scope = scope
-    ; prg_kind = kind
-    ; prg_reduce = reduce
-    ; prg_hook = hook
-    ; prg_opaque = opaque
-    }
-
 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 CEphemeron.key
+exception Found of ProgramDecl.t CEphemeron.key
 
 let map_first m =
   try
@@ -436,40 +393,6 @@ let solve_by_tac ?loc name evi t poly uctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
-  let obls, rem = prg.prg_obligations in
-  let cst = match dref with GlobRef.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 inst, ctx' =
-    if not prg.prg_poly (* Not polymorphic *) then
-      (* The universe context was declared globally, we continue
-         from the new global environment. *)
-      let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
-      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
-      Univ.Instance.empty, ctx'
-    else
-      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
-      let uctx = UState.context ctx' in
-      Univ.UContext.instance uctx, ctx'
-  in
-  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
-  let () = if transparent then add_local_hint prg cst in
-  let obls = Array.copy obls in
-  let () = obls.(num) <- obl in
-  let prg = { prg with prg_ctx = ctx' } in
-  let () = ignore (update_obls prg obls (pred rem)) 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) deps None)
-  end
-
 let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
@@ -489,7 +412,7 @@ let rec solve_obligation prg num tac =
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
-  let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
+  let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in
   let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
   let poly = prg.prg_poly in
   let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
@@ -530,8 +453,9 @@ and solve_obligation_by_tac prg obls i tac =
                 prg.prg_poly (Evd.evar_universe_context evd) with
         | None -> None
         | Some (t, ty, ctx) ->
+          let prg = ProgramDecl.set_uctx ~uctx:ctx prg in
+          (* Why is uctx not used above? *)
           let uctx = UState.univ_entry ~poly:prg.prg_poly 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 prg.prg_poly then (
@@ -539,7 +463,7 @@ and solve_obligation_by_tac prg obls i tac =
             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'})
+            Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
           else Some prg
       else None
 
@@ -553,20 +477,20 @@ and solve_prg_obligations prg ?oblset tac =
     | Some s -> set := s;
       (fun i -> Int.Set.mem i !set)
   in
-  let prgref = ref prg in
-  let () =
-    Array.iteri (fun i x ->
+  let prg =
+    Array.fold_left_i (fun i prg 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'
+        match solve_obligation_by_tac prg obls' i tac with
+        | None -> prg
+        | Some prg ->
+          let deps = dependencies obls i in
+          set := Int.Set.union !set deps;
+          decr rem;
+          prg
+      else prg)
+      prg obls'
   in
-    update_obls !prgref obls' !rem
+  update_obls prg obls' !rem
 
 and solve_obligations n tac =
   let prg = get_prog_err n in
@@ -632,7 +556,7 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
                    ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let info = Id.print name ++ str " has type-checked" in
-  let prg = init_prog_info ~opaque name udecl term t uctx [] None [] obls impargs ~poly ~scope ~kind reduce ?hook in
+  let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~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 ".");
@@ -652,9 +576,9 @@ let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
     ?hook ?(opaque = false) notations fixkind =
   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 ~opaque n udecl (Some b) t uctx deps (Some fixkind)
-       notations obls imps ~poly ~scope ~kind reduce ?hook
+    (fun  (n, b, t, impargs, obls) ->
+     let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind)
+       notations obls ~impargs ~poly ~scope ~kind reduce ?hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
@@ -682,10 +606,10 @@ let admit_prog prg =
               (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
-              obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
+              obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
         | Some _ -> ())
       obls;
-    ignore(update_obls prg obls 0)
+    ignore(DeclareObl.update_obls prg obls 0)
 
 let rec admit_all_obligations () =
   let prg = try Some (get_any_prog ()) with NoObligations _ -> None in