Hint_db (p.coq-core.8.17.1.doc.coq-core.tactics.Hints.Hint

Sourcetype t

Sourceval empty : ?name:hint_db_name -> TransparentState.t -> bool -> t

Sourceval 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

Source

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.

Source

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.

Sourceval remove_one : Environ.env -> Names.GlobRef.t -> t -> t

Sourceval remove_list : Environ.env -> Names.GlobRef.t list -> t -> t

Source

val iter : 
  (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) ->
  t ->
  unit

Source

val fold : 
  (Names.GlobRef.t option ->
    hint_mode array list ->
    FullHint.t list ->
    'a ->
    'a) ->
  t ->
  'a ->
  'a

Sourceval use_dn : t -> bool

Sourceval transparent_state : t -> TransparentState.t

Sourceval set_transparent_state : t -> TransparentState.t -> t

Sourceval add_cut : hints_path -> t -> t

Sourceval cut : t -> hints_path

Sourceval unfolds : t -> Names.Id.Set.t * Names.Cset.t

Sourceval add_modes : hint_mode array list Names.GlobRef.Map.t -> t -> t

Sourceval modes : t -> hint_mode array list Names.GlobRef.Map.t