Module Hints

General functions.
exception Bound
val decompose_app_bound : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t * EConstr.constr array
type debug =
| Debug
| Info
| Off
val secvars_of_hyps : ('c, 't) Context.Named.pt -> Names.Id.Pred.t
val empty_hint_info : 'a Typeclasses.hint_info_gen
type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
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 Names.evaluable_global_reference
| Extern of Genarg.glob_generic_argument
type hint
type raw_hint = EConstr.constr * EConstr.types * Univ.ContextSet.t
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
type 'a with_metadata = private {
pri : int;

A number lower is higher priority

poly : bool;

Is the hint polymorpic and hence should be refreshed at each application

pat : Pattern.constr_pattern option;

A pattern for the concl of the Goal

name : hints_path_atom;

A potential name to refer to the hint

db : string option;

The database from which the hint comes

secvars : Names.Id.Pred.t;

The set of section variables the hint depends on

code : 'a;

the tactic to apply when the concl matches pat

}
type full_hint = hint with_metadata
type search_entry
type hint_entry
type reference_or_constr =
| HintsReference of Libnames.qualid
| HintsConstr of Constrexpr.constr_expr
type hint_mode =
| ModeInput
| ModeNoHeadEvar
| ModeOutput
type 'a hints_transparency_target =
| HintsVariables
| HintsConstants
| HintsReferences of 'a list
type hints_expr =
| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
| HintsResolveIFF of bool * Libnames.qualid list * int option
| HintsImmediate of reference_or_constr list
| HintsUnfold of Libnames.qualid list
| HintsTransparency of Libnames.qualid hints_transparency_target * bool
| HintsMode of Libnames.qualid * hint_mode list
| HintsConstructors of Libnames.qualid list
| HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
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 =
| IsGlobRef of Names.GlobRef.t
| IsConstr of EConstr.constr * Univ.ContextSet.t
type hints_entry =
| HintsResolveEntry of (Typeclasses.hint_info * bool * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of Names.evaluable_global_reference list
| HintsTransparencyEntry of Names.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 searchtable_map : hint_db_name -> hint_db
val searchtable_add : (hint_db_name * hint_db) -> unit
val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : bool -> 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 interp_hints : poly:bool -> hints_expr -> hints_entry
val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool -> (bool * bool) -> Environ.env -> Evd.evar_map -> (Evd.evar_map * EConstr.constr) -> hint_term
val make_exact_entry : Environ.env -> Evd.evar_map -> Typeclasses.hint_info -> poly:bool -> ?⁠name:hints_path_atom -> (EConstr.constr * EConstr.types * Univ.ContextSet.t) -> hint_entry
val make_apply_entry : Environ.env -> Evd.evar_map -> (bool * bool * bool) -> Typeclasses.hint_info -> poly:bool -> ?⁠name:hints_path_atom -> (EConstr.constr * EConstr.types * Univ.ContextSet.t) -> hint_entry
val make_resolves : Environ.env -> Evd.evar_map -> (bool * bool * bool) -> Typeclasses.hint_info -> poly:bool -> ?⁠name:hints_path_atom -> hint_term -> hint_entry list
val make_resolve_hyp : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> hint_entry list
val make_extern : int -> Pattern.constr_pattern option -> Genarg.glob_generic_argument -> hint_entry
val run_hint : hint -> ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast

This function is for backward compatibility only, not to use in newly written code.

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 pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t
val pr_applicable_hint : Proof_global.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
val pr_hint : Environ.env -> Evd.evar_map -> hint -> Pp.t