Merge PR #11731: [proof] Miscellaneous refactorings

Reviewed-by: SkySkimmer
Reviewed-by: gares

28 files changed, 480 insertions, 415 deletions

diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
new file mode 100644
index 0000000000..6928925e54
--- /dev/null
+++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then
+
+    equations_CI_REF=proof+more_naming_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    rewriter_CI_REF=proof+more_naming_unif
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+    elpi_CI_REF=proof+more_naming_unif
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 307214089f..2fdca15552 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,12 +1,12 @@
-let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
   let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
-      ~opaque ~poly sigma udecl ~types:tyopt ~body in
+      ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
-  let ubinders = Evd.universe_binders sigma in
+  let ubind = Evd.universe_binders sigma in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
   edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None []
+    ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 7bddbc994f..446026c4c8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -295,8 +295,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       ~name:new_princ_name ~hook_data
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
-      UnivNames.empty_binders
-      entry [] in
+      ~ubind:UnivNames.empty_binders
+      ~impargs:[]
+      entry in
   ()
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4bab3bd6ea..ded159e484 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -187,7 +187,7 @@ let interp_sort_info ?loc evd l =
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
 
-type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
+type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
 
 type inference_flags = {
   use_typeclasses : bool;
@@ -247,17 +247,16 @@ let apply_typeclasses ~program_mode env sigma frozen fail_evar =
     else sigma in
   sigma
 
-let apply_inference_hook hook env sigma frozen = match frozen with
+let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with
 | FrozenId _ -> sigma
 | FrozenProgress (lazy (_, pending)) ->
   Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
-      try
-        let sigma, c = hook env sigma evk in
+      match hook env sigma evk with
+      | Some (sigma, c) ->
         Evd.define evk c sigma
-      with Exit ->
-        sigma
+      | None -> sigma
     else
       sigma) pending sigma
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 700ca93c33..abbb745161 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,6 @@ type typing_constraint =
   | OfType of types (** A term of the expected type *)
   | WithoutTypeConstraint (** A term of unknown expected type *)
 
-type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
-
 type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
@@ -103,13 +101,17 @@ val understand_ltac : inference_flags ->
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
 
+(** [hook env sigma ev] returns [Some (sigma', term)] if [ev] can be
+   instantiated with a solution, [None] otherwise. Used to extend
+   [solve_remaining_evars] below. *)
+type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
+
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)
 (* For simplicity, it is assumed that current map has no other evars
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
-
 val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
   env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map
 
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/tactics/abstract.ml b/tactics/abstract.ml
index 9b0a323078..e85d94cd72 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context sigma in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
diff --git a/tactics/declare.ml b/tactics/declare.ml
index de3c731d9b..5e6f78be6f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -351,11 +351,11 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
-let inline_private_constants ~univs env ce =
+let inline_private_constants ~uctx env ce =
   let body, eff = Future.force ce.proof_entry_body in
   let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
-  let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in
-  cb, univs
+  let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
+  cb, uctx
 
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
@@ -382,13 +382,13 @@ let declare_variable ~name ~kind d =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let ((body, uctx), eff) = Future.force de.proof_entry_body in
+      let ((body, body_ui), eff) = Future.force de.proof_entry_body in
       let () = export_side_effects eff in
-      let poly, univs = match de.proof_entry_universes with
+      let poly, entry_ui = match de.proof_entry_universes with
         | Monomorphic_entry uctx -> false, uctx
         | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
-      let univs = Univ.ContextSet.union uctx univs in
+      let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = declare_universe_context ~poly univs in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f87d08fc8b..0068b9842a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -108,11 +108,11 @@ val declare_private_constant
   -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
-(** [inline_private_constants ~sideff ~univs env ce] will inline the
+(** [inline_private_constants ~sideff ~uctx env ce] will inline the
    constants in [ce]'s body and return the body plus the updated
    [UState.t]. *)
 val inline_private_constants
-  :  univs:UState.t
+  :  uctx:UState.t
   -> Environ.env
   -> Evd.side_effects proof_entry
   -> Constr.t * UState.t
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 438892e75e..b228a04298 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -116,31 +116,31 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac =
-  let evd = Evd.from_ctx ctx in
+let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac =
+  let evd = Evd.from_ctx uctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
   let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   let pf, status = by tac pf in
   let open Proof_global in
-  let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
   match entries with
   | [entry] ->
-    entry, status, universes
+    entry, status, uctx
   | _ ->
     CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
 
-let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
-  let cb, univs =
-    if side_eff then Declare.inline_private_constants ~univs env ce
+  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then Declare.inline_private_constants ~uctx env ce
     else
       (* GG: side effects won't get reset: no need to treat their universes specially *)
       let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
   in
-  cb, status, univs
+  cb, ce.Declare.proof_entry_type, status, univs
 
 let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Save the initial side-effects to restore them afterwards. We set the
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 3cf3a13262..c49e997757 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -64,8 +64,8 @@ val use_unification_heuristics : unit -> bool
 val build_constant_by_tactic
   :  name:Id.t
   -> ?opaque:Proof_global.opacity_flag
-  -> UState.t
-  -> named_context_val
+  -> uctx:UState.t
+  -> sign:named_context_val
   -> poly:bool
   -> EConstr.types
   -> unit Proofview.tactic
@@ -74,11 +74,11 @@ val build_constant_by_tactic
 val build_by_tactic
   :  ?side_eff:bool
   -> env
-  -> UState.t
+  -> uctx:UState.t
   -> poly:bool
-  -> EConstr.types
+  -> typ:EConstr.types
   -> unit Proofview.tactic
-  -> constr * bool * UState.t
+  -> constr * types option * bool * UState.t
 
 val refine_by_tactic
   :  name:Id.t
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7d59a18494..7fd1634dcf 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -27,8 +27,7 @@ module NamedDecl = Context.Named.Declaration
 type proof_object =
   { name : Names.Id.t
   ; entries : Evd.side_effects Declare.proof_entry list
-  ; poly : bool
-  ; universes: UState.t
+  ; uctx: UState.t
   ; udecl : UState.universe_decl
   }
 
@@ -159,7 +158,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
   in
   let fpl, univs = Future.split2 fpl in
-  let universes = if poly || now then Future.force univs else initial_euctx in
+  let uctx = if poly || now then Future.force univs else initial_euctx in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -167,7 +166,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     let { Proof.sigma } = Proof.data proof in
     Evd.existential_opt_value0 sigma k in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
-    (UState.subst universes) in
+    (UState.subst uctx) in
 
   let make_body =
     if poly || now then
@@ -182,7 +181,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
         let used_univs_typ = Vars.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.univ_entry ~poly initial_euctx in
-          let ctx = constrain_variables universes in
+          let ctx = constrain_variables uctx in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
              the body.  So we keep the two sets distinct. *)
@@ -192,7 +191,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
           (initunivs, typ), ((body, univs), eff)
         else if poly && opaque && private_poly_univs () then
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let universes = UState.restrict universes used_univs in
+          let universes = UState.restrict uctx used_univs in
           let typus = UState.restrict universes used_univs_typ in
           let udecl = UState.check_univ_decl ~poly typus udecl in
           let ubody = Univ.ContextSet.diff
@@ -207,7 +206,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              the actually used universes.
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = UState.restrict universes used_univs in
+          let ctx = UState.restrict uctx used_univs in
           let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in
@@ -215,7 +214,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     else
       fun t p ->
         (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = UState.univ_entry ~poly:false universes in
+        let univctx = UState.univ_entry ~poly:false uctx in
         let t = nf t in
         Future.from_val (univctx, t),
         Future.chain p (fun (pt,eff) ->
@@ -240,7 +239,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
   in
   let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
-  { name; entries; poly; universes; udecl }
+  { name; entries; uctx; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 8c1bc0def1..f1281d1291 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -33,9 +33,7 @@ type proof_object =
   (** name of the proof *)
   ; entries : Evd.side_effects Declare.proof_entry list
   (** list of the proof terms (in a form suitable for definitions). *)
-  ; poly : bool
-  (** polymorphic status *)
-  ; universes: UState.t
+  ; uctx: UState.t
   (** universe state *)
   ; udecl : UState.universe_decl
   (** universe declaration *)
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 *)