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. --- tactics/hints.mli | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'tactics/hints.mli') diff --git a/tactics/hints.mli b/tactics/hints.mli index f05988703..7ef7f0185 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -14,10 +14,10 @@ open EConstr open Environ open Decl_kinds open Evd -open Misctypes open Tactypes open Clenv open Pattern +open Typeclasses (** {6 General functions. } *) @@ -33,6 +33,8 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -80,7 +82,7 @@ type hint_mode = | ModeOutput (* Anything *) type hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool @@ -160,8 +162,6 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen - type hint_term = | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t @@ -290,3 +290,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) val add_hints_init : (unit -> unit) -> unit +type nonrec hint_info = hint_info +[@@ocaml.deprecated "Use [Typeclasses.hint_info]"] -- cgit v1.2.3