package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.tactics/Hints/Hint_db/index.html

Module Hints.Hint_dbSource

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.

Sourceval map_all : 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.

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
Sourceval iter : (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) -> t -> unit
Sourceval 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 add_modes : hint_mode array list Names.GlobRef.Map.t -> t -> t
Sourceval modes : t -> hint_mode array list Names.GlobRef.Map.t