From 8b302bfba8f98458087685c8d5fbca2cf647255f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 21 May 2018 10:45:28 +0200 Subject: Move interning the [hint_pattern] outside the Typeclasses hooks. Close #7562. [api] move hint_info ast to tactics. --- pretyping/typeclasses.ml | 6 +++--- pretyping/typeclasses.mli | 16 ++++++++-------- 2 files changed, 11 insertions(+), 11 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 12a944d32..70588b6ad 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -30,7 +30,7 @@ type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen +type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d @@ -80,7 +80,7 @@ type typeclass = { cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * hint_info_expr) option + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; cl_strict : bool; @@ -92,7 +92,7 @@ type typeclasses = typeclass Refmap.t type instance = { is_class: GlobRef.t; - is_info: hint_info_expr; + is_info: hint_info; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2a8e0b874..c78382c82 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -21,7 +21,7 @@ type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen +type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen (** This module defines type-classes *) type typeclass = { @@ -44,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 * hint_info_expr) option * Constant.t option) list; + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -62,7 +62,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance +val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -129,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state val add_instance_hint_hook : (global_reference_or_constr -> GlobRef.t list -> - bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t + bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t val add_instance_hint : global_reference_or_constr -> GlobRef.t list -> - bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit + bool -> hint_info -> Decl_kinds.polymorphic -> unit val remove_instance_hint : GlobRef.t -> 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 : hint_info_expr option -> bool -> GlobRef.t -> unit +val declare_instance : hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. @@ -146,5 +146,5 @@ val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit subinstances and add only the missing ones. *) val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t -> - hint_info_expr -> - (GlobRef.t list * hint_info_expr * constr) list + hint_info -> + (GlobRef.t list * hint_info * constr) list -- cgit v1.2.3