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 -> Names.transparent_state -> 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
val map_eauto : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> full_hint list
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 use_dn : t -> bool
val transparent_state : t -> Names.transparent_state
val set_transparent_state : t -> Names.transparent_state -> t
val add_cut : hints_path -> t -> t
val cut : t -> hints_path
val unfolds : t -> Names.Id.Set.t * Names.Cset.t