diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 22:49:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (patch) | |
| tree | 0fd697ed68507449268811a630a201f7637c3553 /pretyping/typeclasses.mli | |
| parent | 9938aed874d3e15e5d21689ea841bdc3e6ebb40e (diff) | |
Make the typeclass implementation fully compatible with universe polymorphism.
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index a8e90ca17..99cdbd3a3 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,10 @@ type direction = Forward | Backward (** This module defines type-classes *) type typeclass = { + (** The toplevel universe quantification in which the typeclass lives. In + particular, [cl_props] and [cl_context] are quantified over it. *) + cl_univs : Univ.AUContext.t; + (** 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; @@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses +val typeclass_univ_instance : typeclass puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option |