diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 871da55116..800deefda4 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -74,6 +74,9 @@ val is_implicit_arg : hole_kind -> bool val instance_constructor : typeclass -> constr list -> constr * types +(** Resolvability. + Only undefined evars could be marked or checked for resolvability. *) + val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map |