diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 67336b3407..b1db243d67 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -80,7 +80,7 @@ val is_implicit_arg : hole_kind -> bool val instance_constructor : typeclass -> constr list -> constr option * types (** Resolvability. - Only undefined evars could be marked or checked for resolvability. *) + Only undefined evars can be marked or checked for resolvability. *) val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info @@ -89,7 +89,7 @@ val mark_resolvable : evar_info -> evar_info val mark_resolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool -val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> +val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : env -> evar_map -> types -> open_constr |