Module `Hints`

val decompose_app_bound : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t * EConstr.constr array

type 'a hint_ast = | Res_pf of 'a | ERes_pf of 'a | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a | Unfold_nth of Tacred.evaluable_global_reference | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument
type hint = private { hint_term : EConstr.constr; hint_type : EConstr.types; hint_uctx : Univ.ContextSet.t option; hint_clnv : Clenv.clausenv; }
type 'a hints_path_atom_gen = | PathHints of 'a list | PathAny
type hints_path_atom = Names.GlobRef.t hints_path_atom_gen
type hint_db_name = string

module FullHint : sig ... end

type hint_mode = | ModeInput | ModeNoHeadEvar | ModeOutput
type 'a hints_transparency_target = | HintsVariables | HintsConstants | HintsReferences of 'a list
type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen | PathStar of 'a hints_path_gen | PathSeq of 'a hints_path_gen * 'a hints_path_gen | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon
type pre_hints_path = Libnames.qualid hints_path_gen
type hints_path = Names.GlobRef.t hints_path_gen

val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
val path_derivate : hints_path -> hints_path_atom -> hints_path
val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t
val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
val pp_hints_path : hints_path -> Pp.t
val pp_hint_mode : hint_mode -> Pp.t
val glob_hints_path_atom : Libnames.qualid hints_path_atom_gen -> Names.GlobRef.t hints_path_atom_gen
val glob_hints_path : Libnames.qualid hints_path_gen -> Names.GlobRef.t hints_path_gen

module Hint_db : sig ... end

type hint_db = Hint_db.t
type hnf = bool
type hint_term
type hints_entry = | HintsResolveEntry of (Typeclasses.hint_info * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of Tacred.evaluable_global_reference list | HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool | HintsModeEntry of Names.GlobRef.t * hint_mode list | HintsExternEntry of Typeclasses.hint_info * Genarg.glob_generic_argument

val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : locality:Goptions.option_locality -> hint_db_name list -> Names.GlobRef.t list -> unit
val current_db_names : unit -> Util.String.Set.t
val current_pure_db : unit -> hint_db list
val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
val hint_globref : Names.GlobRef.t -> hint_term
val hint_constr : (EConstr.constr * Univ.ContextSet.t option) -> hint_term

val push_resolves : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Hint_db.t -> Hint_db.t

val push_resolve_hyp : Environ.env -> Evd.evar_map -> Names.Id.t -> Hint_db.t -> Hint_db.t

val make_local_hint_db : Environ.env -> Evd.evar_map -> ?⁠ts:TransparentState.t -> bool -> Tactypes.delayed_open_constr list -> hint_db
val make_db_list : hint_db_name list -> hint_db list
val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic: Use around toplevel calls to hint-using tactics, to enable the tracking of non-imported hints. Any tactic calling run_hint must be wrapped this way.

val wrap_hint_warning_fun : Environ.env -> Evd.evar_map -> (Evd.evar_map -> 'a * Evd.evar_map) -> 'a * Evd.evar_map: Variant of the above for non-tactics

val fresh_hint : Environ.env -> Evd.evar_map -> hint -> Evd.evar_map * EConstr.constr
val hint_res_pf : ?⁠with_evars:bool -> ?⁠with_classes:bool -> ?⁠flags:Unification.unify_flags -> hint -> unit Proofview.tactic

val pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t
val pr_applicable_hint : Proof.t -> Pp.t
val pr_hint_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Pp.t
val pr_hint_db_by_name : Environ.env -> Evd.evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t