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 map_none : secvars:Names.Id.Pred.t -> t -> FullHint.t list
val map_all : secvars:Names.Id.Pred.t -> Names.GlobRef.t -> t -> FullHint.t list
val map_existential : Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> FullHint.t list with_mode
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
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 : 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