diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 12 |
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 |