Merge PR #11731: [proof] Miscellaneous refactorings

Reviewed-by: SkySkimmer
Reviewed-by: gares

15 files changed, 416 insertions, 362 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9ed371bcfb..0c9b9c7255 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -691,10 +691,10 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal
+  let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -821,10 +821,10 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal
+  let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -997,13 +997,13 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx
-    (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
-    (compute_dec_tact ind lnamesparrec nparrec)
+  let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
+      ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
+      (compute_dec_tact ind lnamesparrec nparrec)
   in
   ([|ans|], ctx), Evd.empty_side_effects
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b1f7b2a0c3..dafd1cc5e4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -312,29 +312,29 @@ let instance_hook info global imps ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global imps ?hook name decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
   let sigma, entry = DeclareDef.prepare_definition
-      ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in
+      ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
   let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
   Declare.definition_message name;
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
   instance_hook info global imps ?hook (GlobRef.ConstRef kn)
 
-let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name =
+let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook pri global imps (GlobRef.ConstRef cst)
+  instance_hook pri global impargs (GlobRef.ConstRef cst)
 
-let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype =
+let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype =
   let hook { DeclareDef.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
     Impargs.declare_manual_implicits false dref imps;
@@ -345,10 +345,10 @@ let declare_instance_program env sigma ~global ~poly name pri imps univdecl term
   in
   let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in
   let hook = DeclareDef.Hook.make hook in
-  let ctx = Evd.evar_universe_context sigma in
+  let uctx = Evd.evar_universe_context sigma in
   let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
   let _ : DeclareObl.progress =
-    Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls
+    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls
   in ()
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8eff26bae5..dc9c8e2d3c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -204,7 +204,7 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry []
+            ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
         in
         ()
     in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 8a0d0c9d81..ba2c1ac115 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -70,7 +70,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
 
   let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
-      ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in
+      ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in
 
   (ce, evd, udecl, imps)
 
@@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt =
-  let (ce, evd, univdecl, imps as def) =
-    interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt
+let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let (ce, evd, udecl, impargs as def) =
+    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   if program_mode then
     let env = Global.env () in
@@ -97,12 +97,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
     let obls, _, c, cty =
       Obligations.eterm_obligations env name evd 0 c typ
     in
-    let ctx = Evd.evar_universe_context evd in
+    let uctx = Evd.evar_universe_context evd in
     ignore(Obligations.add_definition
-             ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls)
+             ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls)
   else
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
     let kind = Decls.IsDefinition kind in
-    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps)
+    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 8c050b800a..0a70954dd2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -9,22 +9,9 @@
 (************************************************************************)
 
 open Pp
-open CErrors
 open Util
-open Constr
-open Context
-open Vars
-open Termops
-open Declare
 open Names
-open Constrexpr
-open Constrexpr_ops
 open Constrintern
-open Pretyping
-open Evarutil
-open Evarconv
-
-module RelDecl = Context.Rel.Declaration
 
 (* 3c| Fixpoints and co-fixpoints *)
 
@@ -99,7 +86,7 @@ let check_mutuality env evd isfix fixl =
   let names = List.map fst fixl in
   let preorder =
     List.map (fun (id,def) ->
-      (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names))
+      (id, List.filter (fun id' -> not (Id.equal id id') && Termops.occur_var env evd id' def) names))
       fixl in
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -110,13 +97,13 @@ let check_mutuality env evd isfix fixl =
 let interp_fix_context ~program_mode ~cofix env sigma fix =
   let before, after =
     if not cofix
-    then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
+    then Constrexpr_ops.split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
     else [], fix.Vernacexpr.binders in
   let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
   let sigma, (impl_env', ((env'', ctx'), imps')) =
     interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
   in
-  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
+  let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
@@ -134,8 +121,8 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
 let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs =
-  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
-  let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in
+  let defs = List.map (Vars.subst_vars (List.rev fixnames)) fixdefs in
+  let names = List.map2 (fun id r -> Context.make_annot (Name id) r) fixnames fixrs in
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
 (* Jump over let-bindings. *)
@@ -154,7 +141,7 @@ let compute_possible_guardness_evidences (ctx,_,recindex) =
       List.interval 0 (Context.Rel.nhyps ctx - 1)
 
 type recursive_preentry =
-  Id.t list * Sorts.relevance list * constr option list * types list
+  Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list
 
 (* Wellfounded definition *)
 
@@ -177,9 +164,9 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
           let open UState in
           let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
            if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
-             user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
+             CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
            Some us) fixl None in
-  let sigma, decl = interp_univ_decl_opt env all_universes in
+  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in
   let sigma, (fixctxs, fiximppairs, fixannots) =
     on_snd List.split3 @@
       List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
@@ -188,7 +175,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
     on_snd List.split3 @@
       List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
+  let fixtypes = List.map (fun c -> Evarutil.nf_evar sigma c) fixtypes in
   let fiximps = List.map3
     (fun ctximps cclimps (_,ctx) -> ctximps@cclimps)
     fixctximps fixcclimps fixctxs in
@@ -204,8 +191,8 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
                Typing.solve_evars env sigma app
              with e when CErrors.noncritical e -> sigma, t
            in
-           sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env'
-         else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env')
+           sigma, LocalAssum (Context.make_annot id Sorts.Relevant,fixprot) :: env'
+         else sigma, LocalAssum (Context.make_annot id Sorts.Relevant,t) :: env')
       (sigma,[]) fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
@@ -224,7 +211,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
+  let sigma = Evarconv.solve_unif_constraints_with_heuristics env_rec sigma in
   let sigma = Evd.minimize_universes sigma in
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
@@ -238,7 +225,7 @@ let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
   end
 
 let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
-  check_evars_are_solved ~program_mode:false env evd;
+  Pretyping.check_evars_are_solved ~program_mode:false env evd;
   let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
@@ -257,14 +244,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
         { Lemmas.Recthm.name; typ
-        ; args = List.map RelDecl.get_name ctx; impargs})
+        ; args = List.map Context.Rel.Declaration.get_name ctx; impargs})
       fixnames fixtypes fiximps in
-  let init_tac =
-    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
+  let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
     Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
-      evd (Some(cofix,indexes,init_tac)) thms None in
+      evd (Some(cofix,indexes,init_terms)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
@@ -281,12 +267,12 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let vars, fixdecls, gidx =
     if not cofix then
       let env = Global.env() in
-      let indexes = search_guard env indexes fixdecls in
-      let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
-      let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+      let indexes = Pretyping.search_guard env indexes fixdecls in
+      let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in
+      let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in
       vars, fixdecls, Some indexes
     else (* cofix *)
-      let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+      let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in
       let vars = Vars.universes_of_constr (List.hd fixdecls) in
       vars, fixdecls, None
   in
@@ -294,29 +280,33 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
-  let udecl = Evd.universe_binders evd in
+  let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    List.map4 (fun name body types imps ->
+    List.map4 (fun name body types impargs ->
         let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
-        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
       fixnames fixdecls fixtypes fiximps
   in
-  recursive_message (not cofix) gidx fixnames;
+  Declare.recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
-let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
+let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
+  let open Constrexpr in
+  match v with
   | CStructRec na -> na
   | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
   | CMeasureRec (None,_,_) when not structonly ->
-    user_err Pp.(str "Decreasing argument must be specified in measure clause.")
-  | _ -> user_err Pp.(str
-           "Well-founded induction requires Program Fixpoint or Function.")
+    CErrors.user_err Pp.(str "Decreasing argument must be specified in measure clause.")
+  | _ ->
+    CErrors.user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.")
 
 (* This is a special case: if there's only one binder, we pick it as
    the recursive argument if none is provided. *)
 let adjust_rec_order ~structonly binders rec_order =
-  let rec_order = Option.map (fun rec_order -> match binders, rec_order with
+  let rec_order = Option.map (fun rec_order ->
+      let open Constrexpr in
+      match binders, rec_order with
       | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
         CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
       | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4f9c247b71..3bac0419ef 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -115,7 +115,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -234,7 +234,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
-        let univs = Evd.check_univ_decl ~poly sigma decl in
+        let univs = Evd.check_univ_decl ~poly sigma udecl in
         (*FIXME poly? *)
         let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
         (* FIXME: include locality *)
@@ -258,9 +258,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 def typ
   in
-  let ctx = Evd.evar_universe_context sigma in
-    ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl
-             ~poly evars_typ ctx evars ~hook)
+  let uctx = Evd.evar_universe_context sigma in
+  ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
+           ~poly evars_typ ~uctx evars ~hook)
 
 let out_def = function
   | Some def -> def
@@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty =
 
 let do_program_recursive ~scope ~poly fixkind fixl =
   let cofix = fixkind = DeclareObl.IsCoFixpoint in
-  let (env, rec_sign, pl, evd), fix, info =
+  let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
@@ -311,13 +311,13 @@ let do_program_recursive ~scope ~poly fixkind fixl =
                               ((indexes,i),fixdecls))
         fixl
   end in
-  let ctx = Evd.evar_universe_context evd in
+  let uctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
 
 let do_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index a032ebf3f9..09582f4ef2 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,7 +43,7 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
+let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   let fix_exn = Declare.Internal.get_fix_exn ce in
   let should_suggest = ce.Declare.proof_entry_opaque &&
                        Option.is_empty ce.Declare.proof_entry_secctx in
@@ -56,10 +56,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
     let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
-    let () = DeclareUniv.declare_univ_binders gr udecl in
+    let () = DeclareUniv.declare_univ_binders gr ubind in
     gr
   in
-  let () = maybe_declare_manual_implicits false dref imps in
+  let () = maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
   begin
     match hook_data with
@@ -95,7 +95,7 @@ let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
   if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
-let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body =
+let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
       sigma (fun nf -> nf body, Option.map nf types)
@@ -103,10 +103,10 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~bo
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
-let prepare_parameter ~allow_evars ~poly sigma udecl typ =
+let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
-      sigma (fun nf -> nf typ)
+      sigma (fun nf -> nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, (None(*proof using*), (typ, univs), None(*inline*))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1ff2145c0d..fb1fc9242c 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,9 +44,9 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> UnivNames.universe_binders
+  -> ubind:UnivNames.universe_binders
+  -> impargs:Impargs.manual_implicits
   -> Evd.side_effects Declare.proof_entry
-  -> Impargs.manual_implicits
   -> GlobRef.t
 
 val declare_assumption
@@ -64,12 +64,16 @@ val prepare_definition
   -> ?opaque:bool
   -> ?inline:bool
   -> poly:bool
-  -> Evd.evar_map
-  -> UState.universe_decl
+  -> udecl:UState.universe_decl
   -> types:EConstr.t option
   -> body:EConstr.t
+  -> Evd.evar_map
   -> Evd.evar_map * Evd.side_effects Declare.proof_entry
 
-val prepare_parameter : allow_evars:bool ->
-  poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
-  Evd.evar_map * Entries.parameter_entry
+val prepare_parameter
+  : allow_evars:bool
+  -> poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.types
+  -> Evd.evar_map
+  -> Evd.evar_map * Entries.parameter_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index a081aa3dae..626dcd5d34 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -18,39 +18,96 @@ 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 =
+  { obls : Obligation.t array
+  ; remaining : 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 = obls' ; remaining = 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 +177,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 +262,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
@@ -232,7 +289,7 @@ let progmap_add n prg =
 let progmap_replace prg' =
   Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
 
-let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
+let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
 
 let obligations_message rem =
   if rem > 0 then
@@ -272,7 +329,7 @@ let rec intset_to = function
   | n -> Int.Set.add n (intset_to (pred n))
 
 let obligation_substitution expand prg =
-  let obls, _ = prg.prg_obligations in
+  let obls = prg.prg_obligations.obls in
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
@@ -348,12 +405,12 @@ let declare_definition prg =
   in
   let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
-  let ubinders = UState.universe_binders uctx in
+  let ubind = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
   DeclareDef.declare_definition
-    ~name:prg.prg_name ~scope:prg.prg_scope ubinders
+    ~name:prg.prg_name ~scope:prg.prg_scope ~ubind
     ~kind:Decls.(IsDefinition prg.prg_kind) ce
-    prg.prg_implicits ?hook_data
+    ~impargs:prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -429,12 +486,12 @@ let declare_mutual_definition l =
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
-  let udecl = UnivNames.empty_binders in
+  let ubind = UnivNames.empty_binders in
   let kns =
     List.map4
-      (fun name body types imps ->
+      (fun name body types impargs ->
          let ce = Declare.definition_entry ~opaque ~types ~univs body in
-         DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps)
+         DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
@@ -448,7 +505,8 @@ let declare_mutual_definition l =
   dref
 
 let update_obls prg obls rem =
-  let prg' = {prg with prg_obligations = (obls, rem)} in
+  let prg_obligations = { obls; remaining = rem } in
+  let prg' = {prg with prg_obligations} in
   progmap_replace prg';
   obligations_message rem;
   if rem > 0 then Remain rem
@@ -478,6 +536,17 @@ let dependencies obls n =
     obls;
   !res
 
+let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
+  let obls = Array.copy obls in
+  let () = obls.(num) <- obl in
+  let prg = { prg with prg_ctx = uctx } 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
+
 type obligation_qed_info =
   { name : Id.t
   ; num : int
@@ -489,7 +558,7 @@ let obligation_terminator entries uctx { name; num; auto } =
   | [entry] ->
     let env = Global.env () in
     let ty = entry.Declare.proof_entry_type in
-    let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in
+    let body, uctx = Declare.inline_private_constants ~uctx env entry in
     let sigma = Evd.from_ctx uctx in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (* Declare the obligation ourselves and drop the hook *)
@@ -498,7 +567,7 @@ let obligation_terminator entries uctx { name; num; auto } =
     let body = EConstr.to_constr sigma (EConstr.of_constr body) in
     let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
     let ctx = Evd.evar_universe_context sigma in
-    let obls, rem = prg.prg_obligations in
+    let { obls; remaining=rem } = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
       match obl.obl_status, entry.Declare.proof_entry_opaque with
@@ -516,8 +585,6 @@ let obligation_terminator entries uctx { name; num; auto } =
     in
     let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in
     let (defined, obl) = declare_obligation prg obl body ty uctx in
-    let obls = Array.copy obls in
-    let () = obls.(num) <- obl in
     let prg_ctx =
       if prg.prg_poly then (* Polymorphic *)
         (* We merge the new universes and constraints of the
@@ -531,15 +598,38 @@ let obligation_terminator entries uctx { name; num; auto } =
         if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
         else ctx
     in
-    let prg = {prg with prg_ctx} in
-    ignore (update_obls prg obls (pred rem));
-    if pred rem > 0 then
-      let deps = dependencies obls num in
-      if not (Int.Set.is_empty deps) then
-        ignore (auto (Some name) deps None)
+    update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
   | _ ->
     CErrors.anomaly
       Pp.(
         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; remaining=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
+  update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 6e7700a28a..4e20c7c192 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -13,61 +13,101 @@ 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 =
+  { obls : Obligation.t array
+  ; remaining : 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 +119,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/lemmas.ml b/vernac/lemmas.ml
index c2cf7a5ec4..7782ff8ac9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -144,18 +144,22 @@ let rec_tac_initializer finite guard thms snl =
 let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
-  | Some (finite,guard,init_tac) ->
+  | Some (finite,guard,init_terms) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
-    Some (match init_tac with
-        | None ->
-          Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
-        | Some tacl ->
-          Tacticals.New.tclTHENS rec_tac
-            List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms)
-      ),guard
+    let term_tac =
+      match init_terms with
+      | None ->
+        List.map intro_tac thms
+      | Some init_terms ->
+        (* This is the case for hybrid proof mode / definition
+           fixpoint, where terms for some constants are given with := *)
+        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
+        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
+    in
+    Tacticals.New.tclTHENS rec_tac term_tac, guard
   | None ->
     let () = match thms with [_] -> () | _ -> assert false in
-    Some (intro_tac (List.hd thms)), [] in
+    intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _}::other_thms ->
@@ -170,9 +174,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
            } in
     let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
     pf_map (Proof_global.map_proof (fun p ->
-        match init_tac with
-        | None -> p
-        | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
+        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
 (************************************************************************)
 (* Commom constant saving path, for both Qed and Admitted               *)
@@ -196,10 +198,8 @@ module MutualEntry : sig
   val declare_mutdef
     (* Common to all recthms *)
     : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-    -> poly:bool
     -> uctx:UState.t
     -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
-    -> udecl:UState.universe_decl
     (* Only for the first constant, introduced by compat *)
     -> ubind:UnivNames.universe_binders
     -> name:Id.t
@@ -259,7 +259,7 @@ end = struct
         Pp.(str "Not a proof by induction: " ++
             Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
 
-  let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name ?typ ~impargs ~info mutpe i =
+  let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i =
     let { Info.hook; compute_guard; scope; kind; _ } = info in
     match mutpe with
     | NoBody pe ->
@@ -267,7 +267,7 @@ end = struct
     | Single pe ->
       (* We'd like to do [assert (i = 0)] here, however this codepath
          is used when declaring mutual cofixpoints *)
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
     | Mutual pe ->
       (* if typ = None , we don't touch the type; used in the base case *)
       let pe =
@@ -278,19 +278,20 @@ end = struct
       in
       let pe = Declare.Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
 
-  let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } =
+  let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } =
+    (* At some point make this a single iteration *)
     (* At some point make this a single iteration *)
     (* impargs here are special too, fixed in upcoming PRs *)
     let impargs = info.Info.impargs in
-    let r = declare_mutdef ?fix_exn ~poly ~info ~udecl ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in
+    let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in
     (* Before we used to do this, check if that's right *)
     let ubind = UnivNames.empty_binders in
     let rs =
       List.map_i (
         fun i { Recthm.name; typ; impargs } ->
-          declare_mutdef ?fix_exn ~poly ~udecl ~info ~ubind ?hook_data ~uctx ~name ~typ ~impargs entry i) 1 info.Info.other_thms
+          declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
 end
 
@@ -318,11 +319,11 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~name ~poly ~info ~uctx ~udecl pe =
+let finish_admitted ~name ~info ~uctx pe =
   let mutpe = MutualEntry.variable ~info pe in
   let ubind = UnivNames.empty_binders in
   let _r : Names.GlobRef.t list =
-    MutualEntry.declare_mutdef ~uctx ~poly ~udecl ~ubind ~name mutpe in
+    MutualEntry.declare_mutdef ~uctx ~ubind ~name mutpe in
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
@@ -338,7 +339,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in
-  finish_admitted ~name ~poly ~info:lemma.info ~uctx:universes ~udecl (sec_vars, (typ, ctx), None)
+  finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -354,17 +355,17 @@ let finish_proved idopt po info =
   let open Proof_global in
   let { Info.hook } = info in
   match po with
-  | { name; entries=[const]; universes; udecl; poly } ->
+  | { name; entries=[const]; uctx; udecl } ->
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
       let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
-      let hook_data = Option.map (fun hook -> hook, universes, []) hook in
-      let ubind = UState.universe_binders universes in
+      let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+      let ubind = UState.universe_binders uctx in
       let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~fix_exn ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe
+        MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe
       in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
@@ -437,7 +438,7 @@ let finalize_proof idopt proof_obj proof_info =
   | Regular ->
     finish_proved idopt proof_obj proof_info
   | End_obligation oinfo ->
-    DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo
+    DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
   | End_derive { f ; name } ->
     finish_derived ~f ~name ~idopt ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
@@ -453,7 +454,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt =
 (***********************************************************************)
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
-  let { name; entries; universes; udecl; poly } = proof in
+  let { name; entries; uctx; udecl } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -463,8 +464,8 @@ let save_lemma_admitted_delayed ~proof ~info =
   let typ = match proof_entry_type with
     | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement");
     | Some typ -> typ in
-  let ctx = UState.univ_entry ~poly universes in
+  let ctx = UState.univ_entry ~poly uctx in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~name ~poly ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None)
+  finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None)
 
 let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 79fdfe37de..471c955311 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -95,7 +95,7 @@ val start_dependent_lemma
 
 type lemma_possible_guards = int list list
 
-(** Pretty much internal, only used in ComFixpoint *)
+(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
@@ -103,7 +103,7 @@ val start_lemma_with_initialization
   -> kind:Decls.logical_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
-  -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
+  -> (bool * lemma_possible_guards * Constr.t option list option) option
   -> Recthm.t list
   -> int list option
   -> t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index d6ce1036b9..f449cb02f1 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,72 +285,28 @@ 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;
+      if (CEphemeron.get v).prg_obligations.remaining > 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
     ProgMap.iter (fun _ v ->
-                  if snd (CEphemeron.get v).prg_obligations > 0 then
-                    raise (Found v)) m;
+        if (CEphemeron.get v).prg_obligations.remaining > 0 then
+          raise (Found v)) m;
     assert(false)
   with Found x -> x
 
@@ -416,16 +373,14 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego
     Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl ();
             str "This will become an error in the future"])
 
-let solve_by_tac ?loc name evi t poly ctx =
-  (* spiwack: the status is dropped. *)
+let solve_by_tac ?loc name evi t poly uctx =
   try
-    let (entry,_,ctx') =
-      Pfedit.build_constant_by_tactic
-        ~name ~poly ctx evi.evar_hyps evi.evar_concl t in
+    (* the status is dropped. *)
     let env = Global.env () in
-    let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in
-    Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body);
-    Some (body, entry.Declare.proof_entry_type, ctx')
+    let body, types, _, uctx =
+      Pfedit.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
+    Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
+    Some (body, types, uctx)
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = Exninfo.capture exn in
@@ -438,43 +393,9 @@ let solve_by_tac ?loc name evi t poly ctx =
     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
+  let { obls; remaining=rem } = prg.prg_obligations in
   let obl = obls.(num) in
   let remaining = deps_remaining obls obl.obl_deps in
   let () =
@@ -491,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
@@ -502,7 +423,7 @@ let rec solve_obligation prg num 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
+  let { obls; remaining } = prg.prg_obligations in
     if num >= 0 && num < Array.length obls then
       let obl = obls.(num) in
         match obl.obl_body with
@@ -532,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 (
@@ -541,13 +463,13 @@ 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
 
 and solve_prg_obligations prg ?oblset tac =
-  let obls, rem = prg.prg_obligations in
-  let rem = ref rem in
+  let { obls; remaining } = prg.prg_obligations in
+  let rem = ref remaining in
   let obls' = Array.copy obls in
   let set = ref Int.Set.empty in
   let p = match oblset with
@@ -555,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
@@ -579,10 +501,10 @@ and solve_all_obligations tac =
 
 and try_solve_obligation n prg tac =
   let prg = get_prog prg in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining } = 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))
+    | Some prg' -> ignore(update_obls prg' obls' (pred remaining))
     | None -> ()
 
 and try_solve_obligations n tac =
@@ -595,9 +517,9 @@ and auto_solve_obligations n ?oblset tac : progress =
 open Pp
 let show_obligations_of_prg ?(msg=true) prg =
   let n = prg.prg_name in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = prg.prg_obligations in
   let showed = ref 5 in
-    if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
+    if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x ->
                    match x.obl_body with
                    | None ->
@@ -630,12 +552,12 @@ let show_term n =
              Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
-let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
+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 univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in
-  let obls,_ = prg.prg_obligations 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 ".");
     let cst = DeclareObl.declare_definition prg in
@@ -649,14 +571,14 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
         | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res
         | _ -> res)
 
-let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
+let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
                            ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?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 univdecl (Some b) t ctx 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 ->
@@ -672,7 +594,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
     in ()
 
 let admit_prog prg =
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = prg.prg_obligations in
   let obls = Array.copy obls in
     Array.iteri
       (fun i x ->
@@ -684,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
@@ -709,7 +631,7 @@ let next_obligation n tac =
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
   in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = 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
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 6a2eb1472e..101958072a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -51,9 +51,9 @@ val default_tactic : unit Proofview.tactic ref
 val add_definition
   :  name:Names.Id.t
   -> ?term:constr -> types
-  -> UState.t
-  -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
-  -> ?implicits:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> ?udecl:UState.universe_decl (* Universe binders and constraints *)
+  -> ?impargs:Impargs.manual_implicits
   -> poly:bool
   -> ?scope:DeclareDef.locality
   -> ?kind:Decls.definition_object_kind
@@ -65,9 +65,10 @@ val add_definition
   -> DeclareObl.progress
 
 val add_mutual_definitions
+  (* XXX: unify with MutualEntry *)
   : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list
-  -> UState.t
-  -> ?univdecl:UState.universe_decl
+  -> uctx:UState.t
+  -> ?udecl:UState.universe_decl
   (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 295db70bc9..8a4522296f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -473,11 +473,14 @@ let program_inference_hook env sigma ev =
     let concl = evi.Evd.evar_concl in
     if not (Evarutil.is_ground_env sigma env &&
             Evarutil.is_ground_term sigma concl)
-    then raise Exit;
-    let c, _, ctx =
-      Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac
-    in Evd.set_universe_context sigma ctx, EConstr.of_constr c
-  with Logic_monad.TacticFailure e when noncritical e ->
+    then None
+    else
+      let c, _, _, ctx =
+        Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
+      in
+      Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
+  with
+  | Logic_monad.TacticFailure e when noncritical e ->
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
@@ -493,15 +496,10 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
     let ids = List.map Context.Rel.Declaration.get_name ctx in
     check_name_freshness scope id;
-    (* XXX: The nf_evar is critical !! *)
-    evd, (id.CAst.v,
-          (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
-           (ids, imps @ imps'))))
+    evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps'))))
       evd thms in
   let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  (* XXX: This nf_evar is critical too!! We are normalizing twice if
-     you look at the previous lines... *)
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
       { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
@@ -1623,12 +1621,11 @@ let get_nth_goal ~pstate n =
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
 
-exception NoHyp
-
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
 let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
+  let exception NoHyp in
   let open Context.Named.Declaration in
   try
     (* Fallback early to globals *)