Merge PR #11818: [proof] Further consolidation of the regular declaration path

Ack-by: Matafou
Reviewed-by: SkySkimmer

1 files changed, 5 insertions, 5 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3bac0419ef..56780d00a6 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = DeclareDef.Hook.make (hook sigma) in
-  Obligations.check_evars env sigma;
+  RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 def typ
+    RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
@@ -281,15 +281,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
     (* Solve remaining evars *)
   let evd = nf_evar_map_undefined evd in
-  let collect_evars id def typ imps =
+  let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
-      Obligations.eterm_obligations env id evm
+      RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    (id, def, typ, imps, evars)
+    ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in