Module Hints.Hint_db

type t
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 : Environ.env -> secvars:Names.Id.Pred.t -> Names.GlobRef.t -> t -> FullHint.t list

All hints associated to the reference

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_eauto_modes : Environ.env -> Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> (mode_restriction NeList.t option * FullHint.t list) option

As map_eauto, but returns the nonempty list of distinct matching mode restrictions in lookup order, including the evars frozen by each restriction. The entire result is None when modes are declared but no mode matches. The first component of the result is None if no modes are declared.

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 : Environ.env -> hints_path -> t -> t
val cut : t -> hints_path
val add_modes : Modes.t -> t -> t
val modes : t -> Modes.t
val find_mode : Environ.env -> Names.GlobRef.t -> t -> hint_mode array list