diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:46:18 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 12:58:15 +0200 |
commit | 81545ec98255e644be589d34a521924549e9e2fa (patch) | |
tree | 65ab59d21e680a00e379deffa440f038b5d0c121 /pretyping/typeclasses.mli | |
parent | 0f107c8a747af6bdb40d70d80236f84b325dc35d (diff) |
[api] Move `hint_info_expr` to `Typeclasses`.
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r-- | pretyping/typeclasses.mli | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b80c28711..e50d90b15 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,13 @@ open Environ type direction = Forward | Backward +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + (** This module defines type-classes *) type typeclass = { (** The toplevel universe quantification in which the typeclass lives. In @@ -37,7 +44,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; + cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -55,8 +62,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> - global_reference -> instance +val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -123,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state val add_instance_hint_hook : (global_reference_or_constr -> global_reference list -> - bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t + bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t val remove_instance_hint_hook : (global_reference -> unit) Hook.t val add_instance_hint : global_reference_or_constr -> global_reference list -> - bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit + bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit 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 -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit +val declare_instance : hint_info_expr option -> bool -> global_reference -> unit (** Build the subinstances hints for a given typeclass object. @@ -140,5 +146,5 @@ val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_refere subinstances and add only the missing ones. *) val build_subclasses : check:bool -> env -> evar_map -> global_reference -> - Vernacexpr.hint_info_expr -> - (global_reference list * Vernacexpr.hint_info_expr * constr) list + hint_info_expr -> + (global_reference list * hint_info_expr * constr) list |