diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c2f046440..c9ee9adf0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -24,19 +24,19 @@ open Util (* This module defines type-classes *) type typeclass = { - (* The class implementation: a record parameterized by the context with defs in it or a definition if + (* The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : global_reference; + cl_impl : global_reference; - (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. + (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass and the global reference gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) cl_props : rel_context; - (* The methods implementations of the typeclass as projections. Some may be undefinable due to + (* The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions. *) cl_projs : (identifier * constant option) list; } @@ -60,7 +60,7 @@ val dest_class_app : env -> constr -> typeclass * constr list (* Just return None if not a class *) val class_of_constr : constr -> typeclass option - + val instance_impl : instance -> constant val is_class : global_reference -> bool @@ -82,7 +82,7 @@ val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : 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 : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs val resolve_one_typeclass : env -> evar_map -> types -> open_constr |