Module `Hints.Hint_db`

val empty : ?⁠name:hint_db_name -> TransparentState.t -> bool -> t
val map_none : secvars:Names.Id.Pred.t -> t -> FullHint.t 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 -> FullHint.t list: All hints associated to the reference

val map_eauto : Environ.env -> Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> FullHint.t list with_mode: All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. Returns a ModeMismatch if there are declared modes and none matches.

val map_auto : Environ.env -> Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> FullHint.t list: All hints associated to the reference. Precondition: no evars should appear in the arguments, so no modes are checked.

val remove_one : Environ.env -> Names.GlobRef.t -> t -> t
val remove_list : Environ.env -> Names.GlobRef.t list -> t -> t
val iter : (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) -> t -> unit
val fold : (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> 'a -> 'a) -> t -> 'a -> 'a
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