package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val stats : bool Pervasives.ref
val share : bool Pervasives.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 -> 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 = {
  1. i_flags : RedFlags.reds;
  2. i_cache : 'a infos_cache;
}
val ref_value_cache : 'a infos -> table_key -> 'a option
val create : ('a infos -> Term.constr -> 'a) -> RedFlags.reds -> Environ.env -> (Term.existential -> Term.constr option) -> 'a infos
val evar_value : 'a infos_cache -> Term.existential -> Term.constr option
val info_env : 'a infos -> Environ.env
val info_flags : 'a infos -> RedFlags.reds
type fconstr
type fterm =
  1. | FRel of int
  2. | FAtom of Term.constr
  3. | FCast of fconstr * Term.cast_kind * fconstr
  4. | FFlex of table_key
  5. | FInd of Names.inductive Term.puniverses
  6. | FConstruct of Names.constructor Term.puniverses
  7. | FApp of fconstr * fconstr array
  8. | FProj of Names.projection * fconstr
  9. | FFix of Term.fixpoint * fconstr Esubst.subs
  10. | FCoFix of Term.cofixpoint * fconstr Esubst.subs
  11. | FCaseT of Term.case_info * Term.constr * fconstr * Term.constr array * fconstr Esubst.subs
  12. | FLambda of int * (Names.Name.t * Term.constr) list * Term.constr * fconstr Esubst.subs
  13. | FProd of Names.Name.t * fconstr * fconstr
  14. | FLetIn of Names.Name.t * fconstr * fconstr * Term.constr * fconstr Esubst.subs
  15. | FEvar of Term.existential * fconstr Esubst.subs
  16. | FLIFT of int * fconstr
  17. | FCLOS of Term.constr * fconstr Esubst.subs
  18. | FLOCKED
type stack_member =
  1. | Zapp of fconstr array
  2. | ZcaseT of Term.case_info * Term.constr * Term.constr array * fconstr Esubst.subs
  3. | Zproj of int * int * Names.constant
  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 zip_term : (fconstr -> Term.constr) -> Term.constr -> stack -> Term.constr
val eta_expand_stack : stack -> stack
val inject : Term.constr -> fconstr
val mk_atom : Term.constr -> fconstr
val mk_red : fterm -> fconstr
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> Term.constr
type clos_infos = fconstr infos
val create_clos_infos : ?evars:(Term.existential -> Term.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 norm_val : clos_infos -> fconstr -> Term.constr
val whd_val : clos_infos -> fconstr -> Term.constr
val whd_stack : clos_infos -> fconstr -> stack -> fconstr * stack
val eta_expand_ind_stack : Environ.env -> Names.inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack
val unfold_reference : clos_infos -> 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 -> Term.constr array -> fconstr array
val kni : clos_infos -> fconstr -> stack -> fconstr * stack
val knr : clos_infos -> fconstr -> stack -> fconstr * stack
OCaml

Innovation. Community. Security.