diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 9e018f6160..2530f5dfae 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -9,7 +9,6 @@ open Names open Globnames open Term -open Context open Evd open Environ @@ -24,10 +23,10 @@ type typeclass = { (** 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 * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) - cl_props : rel_context; + cl_props : Context.Rel.t; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if @@ -68,7 +67,7 @@ val dest_class_app : env -> constr -> typeclass puniverses * constr list val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option +val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference @@ -102,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> types -> bool -val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> +val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr @@ -120,8 +119,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> bool -> int option -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit -val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) ref -val solve_instantiation_problem : (env -> evar_map -> types -> bool -> open_constr) ref +val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t +val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit |