Module `Hints.Hint_db`

val empty : ?⁠name:hint_db_name -> TransparentState.t -> bool -> t
val find : Names.GlobRef.t -> t -> search_entry
val map_none : secvars:Names.Id.Pred.t -> t -> full_hint list: All hints which have no pattern. * secvars represent the set of section variables that * can be used in the hint.

val map_all : secvars:Names.Id.Pred.t -> Names.GlobRef.t -> t -> full_hint list: All hints associated to the reference

val map_existential : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list: All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net.

val map_eauto : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list: All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net.

val map_auto : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list: All hints associated to the reference, respecting modes if evars appear in the arguments.

val add_one : Environ.env -> Evd.evar_map -> hint_entry -> t -> t
val add_list : Environ.env -> Evd.evar_map -> hint_entry list -> t -> t
val remove_one : Names.GlobRef.t -> t -> t
val remove_list : Names.GlobRef.t list -> t -> t
val iter : (Names.GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> TransparentState.t
val set_transparent_state : t -> TransparentState.t -> t
val add_cut : hints_path -> t -> t
val cut : t -> hints_path
val unfolds : t -> Names.Id.Set.t * Names.Cset.t
val add_modes : hint_mode array list Names.GlobRef.Map.t -> t -> t
val modes : t -> hint_mode array list Names.GlobRef.Map.t