package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val stats : bool ref
val with_stats : 'a Lazy.t -> 'a
val all_opaque : Names.transparent_state
val all_transparent : Names.transparent_state
val is_transparent_variable : Names.transparent_state -> Names.variable -> bool
val is_transparent_constant : Names.transparent_state -> Names.Constant.t -> bool
module type RedFlagsSig = sig ... end
val all : RedFlags.reds
val allnolet : RedFlags.reds
val beta : RedFlags.reds
val betadeltazeta : RedFlags.reds
val betaiota : RedFlags.reds
val betaiotazeta : RedFlags.reds
val betazeta : RedFlags.reds
val delta : RedFlags.reds
val zeta : RedFlags.reds
val nored : RedFlags.reds
val unfold_side_red : RedFlags.reds
type 'a infos_cache
type 'a infos_tab
type !'a infos = {
  1. i_flags : RedFlags.reds;
  2. i_cache : 'a infos_cache;
}
val ref_value_cache : 'a infos -> 'a infos_tab -> table_key -> 'a option
val create : repr:('a infos -> 'a infos_tab -> Constr.constr -> 'a) -> share:bool -> RedFlags.reds -> Environ.env -> (Constr.existential -> Constr.constr option) -> 'a infos
val create_tab : unit -> 'a infos_tab
val evar_value : 'a infos_cache -> Constr.existential -> Constr.constr option
val info_env : 'a infos -> Environ.env
val info_flags : 'a infos -> RedFlags.reds
type fconstr
type stack_member =
  1. | Zapp of fconstr array
  2. | ZcaseT of Constr.case_info * Constr.constr * Constr.constr array * fconstr Esubst.subs
  3. | Zproj of Names.Projection.Repr.t
  4. | Zfix of fconstr * stack
  5. | Zshift of int
  6. | Zupdate of fconstr
and stack = stack_member list
val empty_stack : stack
val append_stack : fconstr array -> stack -> stack
val decomp_stack : stack -> (fconstr * stack) option
val array_of_stack : stack -> fconstr array
val stack_assign : stack -> int -> fconstr -> stack
val stack_args_size : stack -> int
val stack_tail : int -> stack -> stack
val stack_nth : stack -> int -> fconstr
val eta_expand_stack : stack -> stack
val unfold_projection : 'a infos -> Names.Projection.t -> stack_member option
val inject : Constr.constr -> fconstr
val mk_atom : Constr.constr -> fconstr
val mk_red : fterm -> fconstr
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> Constr.constr
type clos_infos = fconstr infos
val create_clos_infos : ?evars:(Constr.existential -> Constr.constr option) -> RedFlags.reds -> Environ.env -> clos_infos
val oracle_of_infos : clos_infos -> Conv_oracle.oracle
val env_of_infos : 'a infos -> Environ.env
val infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos
val whd_stack : clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val eta_expand_ind_stack : Environ.env -> Names.inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack
val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
val eq_table_key : table_key -> table_key -> bool
val lift_fconstr : int -> fconstr -> fconstr
val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos_vect : fconstr Esubst.subs -> Constr.constr array -> fconstr array
val to_constr : Esubst.lift -> fconstr -> Constr.constr