diff options
| author | msozeau | 2011-03-11 17:44:52 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-11 17:44:52 +0000 |
| commit | c70460837f5158325626b9412d8fa0651340b50f (patch) | |
| tree | 623b886c5e05567de8400315a8f0fd35589f6e03 /pretyping/typeclasses.mli | |
| parent | 56f7b49e1f46e495a215d65b7d2acaa03fe3b9cf (diff) | |
Keep information on which fields are subclasses in class declarations,
in preparation for adding forward reasoning to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 3fa1981a3c..1fe955b0c0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -34,8 +34,8 @@ type typeclass = { (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if - no name is provided. *) - cl_projs : (name * constant option) list; + no name is provided. The boolean indicates subclasses. *) + cl_projs : (name * bool * constant option) list; } type instance @@ -61,7 +61,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> constr -> typeclass * constr list (** Just return None if not a class *) -val class_of_constr : constr -> typeclass option +val class_of_constr : constr -> (rel_context * (typeclass * constr list)) option val instance_impl : instance -> global_reference |