diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-23 11:47:43 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-23 11:47:43 +0000 |
| commit | 97f2cb04e369e07dc87dc15d4871b736776614bd (patch) | |
| tree | 47cb65cf28136895ee942f36ba7cde8d214e8217 /pretyping/typeclasses.mli | |
| parent | 81f12192810bdf825cee82658a36214740d1a75b (diff) | |
- Fix bug #1858, Hint Unfold calling the wrong locate function.
- Fix typeclass interface: instance_constructor now takes the instance
constrs as argument to build and return the corresponding term and
type.
- Better typeclass error reporting when defining fixpoints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10975 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c6763a421..43ae592d5 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -60,8 +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 *) -(* Returns the constructor for the given fields of the class and the type constructor. *) -val instance_constructor : typeclass -> (constr list -> constr) * types +(* 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 val resolve_one_typeclass : env -> types -> types (* Raises Not_found *) val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *) |