diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 43ae592d5c..e3c780402f 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -38,7 +38,7 @@ type typeclass = { cl_props : named_context; (* The methods implementations of the typeclass as projections. *) - cl_projs : constant list; + cl_projs : (identifier * constant) list; } type instance @@ -60,6 +60,9 @@ val is_class : global_reference -> bool val class_of_constr : constr -> typeclass option val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *) +val is_instance : global_reference -> bool +val is_method : constant -> bool + (* Returns the term and type for the given instance of the parameters and fields of the type class. *) val instance_constructor : typeclass -> constr list -> constr * types |