diff options
| -rw-r--r-- | toplevel/command.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 3c85868d5..e45005ac3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -880,6 +880,11 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." +let collect_evars_of_term evd c ty = + let evars = Intset.union (evars_of_term c) (evars_of_term ty) in + Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) + evars Evd.empty + let do_program_recursive fixkind fixl ntns = let isfix = fixkind <> Obligations.IsCoFixpoint in let (env, rec_sign, evd), fix, info = @@ -889,17 +894,18 @@ let do_program_recursive fixkind fixl ntns = (* Get the interesting evars, those that were not instanciated *) 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 rec collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - Termops.it_mkNamedLambda_or_LetIn def rec_sign + nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) and typ = - Termops.it_mkNamedProd_or_LetIn typ rec_sign + 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 evd - (List.length rec_sign) - (nf_evar evd def) (nf_evar evd typ) + Obligations.eterm_obligations env id evm + (List.length rec_sign) def typ in (id, def, typ, imps, evars) in let (fixnames,fixdefs,fixtypes) = fix in |