package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type oracle
val empty : oracle
val oracle_order : ('a -> Names.Constant.t) -> oracle -> bool -> 'a Names.tableKey -> 'a Names.tableKey -> bool
type level =
  1. | Expand
  2. | Level of int
  3. | Opaque
val pr_level : level -> Pp.t
val transparent : level
val is_transparent : level -> bool
val get_strategy : oracle -> Names.Constant.t Names.tableKey -> level
val set_strategy : oracle -> Names.Constant.t Names.tableKey -> level -> oracle
val fold_strategy : (Names.Constant.t Names.tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
val get_transp_state : oracle -> TransparentState.t