diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 5 |
2 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d54eaf00ee..0d15034ce5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -364,8 +364,12 @@ let has_typeclasses evd = evd false let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) +let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses (Evd.evars_of evd)) then evd else !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail + +let resolve_one_typeclass env evm t = + !solve_instanciation_problem env evm t diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 60b5da8226..8960ab21b6 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -76,9 +76,12 @@ val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map -val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs +val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> + env -> evar_defs -> evar_defs +val resolve_one_typeclass : env -> evar_map -> types -> constr val register_add_instance_hint : (constant -> int option -> unit) -> unit val add_instance_hint : constant -> int option -> unit val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref +val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref |