Hints
val decompose_app_bound : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t * EConstr.constr array
val secvars_of_hyps : ('c, 't, 'r) Context.Named.pt -> Names.Id.Pred.t
val empty_hint_info : 'a Typeclasses.hint_info_gen
val hint_cat : Libobject.category
Pre-created hint databases
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 Evaluable.t |
| Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument |
val hint_as_term : hint -> UnivGen.sort_context_set option * EConstr.constr
type hints_path_atom = Names.GlobRef.t hints_path_atom_gen
module FullHint : sig ... end
The head may not be bound.
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 path_matches_epsilon : hints_path -> bool
val path_derivate : hints_path -> Names.GlobRef.t option -> hints_path
val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t
val parse_mode : string -> hint_mode
val parse_modes : string -> hint_mode list
val string_of_mode : hint_mode -> string
val glob_hints_path : pre_hints_path -> hints_path
module Hint_db : sig ... end
type hint_db = Hint_db.t
type hints_entry =
| HintsResolveEntry of (Typeclasses.hint_info * hnf * hint_term) list |
| HintsImmediateEntry of hint_term list |
| HintsCutEntry of hints_path |
| HintsUnfoldEntry of Evaluable.t list |
| HintsTransparencyEntry of Evaluable.t 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
create_hint_db local name st use_dn
. st
is a transparency state for unification using this db use_dn
switches the use of the discrimination net for all hints and patterns.
val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : locality:hint_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:hint_locality -> hint_db_name list -> hints_entry -> unit
val hint_globref : Names.GlobRef.t -> hint_term
val hint_constr : (EConstr.constr * UnivGen.sort_context_set option) -> hint_term
A constr which is Hint'ed will be:
val push_resolves : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Hint_db.t -> Hint_db.t
push_resolve_hyp hname htyp db
. used to add an hypothesis to the local hint database; Never raises a user exception; If the hyp cannot be used as a Hint, it is not added.
val push_resolve_hyp : Environ.env -> Evd.evar_map -> Names.Id.t -> Hint_db.t -> Hint_db.t
Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed
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
Printing hints
val pr_searchtable : Environ.env -> Evd.evar_map -> 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