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. --- vernac/classes.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/classes.mli') diff --git a/vernac/classes.mli b/vernac/classes.mli index 27d3a4669..631da8400 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,12 +22,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> hint_info_expr option -> unit +val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - hint_info_expr -> (** priority *) + Hints.hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) ?hook:(GlobRef.t -> unit) -> @@ -51,7 +51,7 @@ val new_instance : ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> - hint_info_expr -> + Hints.hint_info_expr -> Id.t (** Setting opacity *) -- cgit v1.2.3