package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct