package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
val find : Names.GlobRef.t -> t -> search_entry
val map_none : secvars:Names.Id.Pred.t -> t -> full_hint list
val map_all : secvars:Names.Id.Pred.t -> Names.GlobRef.t -> t -> full_hint list
val map_existential : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list with_mode
val map_eauto : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list with_mode
val map_auto : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list
val add_one : Environ.env -> Evd.evar_map -> hint_entry -> t -> t
val add_list : Environ.env -> Evd.evar_map -> hint_entry list -> t -> t
val remove_one : Names.GlobRef.t -> t -> t
val remove_list : Names.GlobRef.t list -> t -> t
val iter : (Names.GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val fold : (Names.GlobRef.t option -> hint_mode array list -> full_hint 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