Merge PR #13393: [proof using] Remove duplicate code, refactor.

Reviewed-by: gares
Ack-by: SkySkimmer

1 files changed, 4 insertions, 8 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3c4a651cf5..0651f3330e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -259,10 +259,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
-  let using = using |> Option.map (fun expr ->
+  let using =
     let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
-    let l = Proof_using.process_expr env sigma expr terms in
-    Names.Id.Set.(List.fold_right add l empty))
+    Option.map (fun using -> Proof_using.definition_using env sigma ~using ~terms) using
   in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
@@ -294,11 +293,8 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
   let evd = nf_evar_map_undefined evd in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
-    let using = using |> Option.map (fun expr ->
-      let terms = [def; typ] in
-      let l = Proof_using.process_expr env evd expr terms in
-      Names.Id.Set.(List.fold_right add l empty))
-    in
+    let terms = [def; typ] in
+    let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in
     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