package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 : 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_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 : hints_path -> t -> t
val cut : t -> hints_path
val unfolds : t -> Names.Id.Set.t * Names.Cset.t
val add_modes : hint_mode array list Names.GlobRef.Map.t -> t -> t
val 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