diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index febfb04947..f9ab283ada 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -216,6 +216,7 @@ let instances r = with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id) let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) +let solve_instanciations_problem = ref (fun _ _ -> assert false) let resolve_typeclass env ev evi (evd, defined as acc) = try @@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types = let evm' = Evd.evars_of evd' in match Evd.evar_body (Evd.find evm' ev) with Evar_empty -> raise Not_found - | Evar_defined c -> c + | Evar_defined c -> Evarutil.nf_evar evm' c else raise Not_found with Exit -> raise Not_found @@ -278,6 +279,8 @@ let destClassApp c = | _ -> None let resolve_typeclasses ?(check=true) env sigma evd = +(* try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *) +(* with _ -> *) let evm = Evd.evars_of evd in let tc_evars = let f ev evi acc = @@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd = (fun ev evi acc -> if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then resolve_typeclass env ev evi acc - else acc) + else acc) (Evd.evars_of evars) (evars, false) in if not progress then evars' else sat (Evarutil.nf_evar_defs evars') - in sat evd - + in sat (Evarutil.nf_evar_defs evd) + let class_of_constr c = let extract_ind c = match kind_of_term c with |