package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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