package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val stats : bool ref
val with_stats : 'a Lazy.t -> 'a
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
module KeyTable : sig ... end
type fconstr
type finvert
type !'a next_native_args = (CPrimitives.arg_kind * 'a) list
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. | Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
  6. | Zshift of int
  7. | Zupdate of fconstr
and stack = stack_member list
val empty_stack : stack
val append_stack : fconstr array -> stack -> stack
val check_native_args : CPrimitives.t -> stack -> bool
val stack_args_size : stack -> int
val eta_expand_stack : stack -> stack
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 optrel =
  1. | Unknown
  2. | KnownR
  3. | KnownI
val relevance_of : fconstr -> optrel
val set_relevance : Sorts.relevance -> fconstr -> unit
type clos_infos
type clos_tab
val create_clos_infos : ?univs:UGraph.t -> ?evars:(Constr.existential -> Constr.constr option) -> RedFlags.reds -> Environ.env -> clos_infos
val oracle_of_infos : clos_infos -> Conv_oracle.oracle
val create_tab : unit -> clos_tab
val info_env : clos_infos -> Environ.env
val info_flags : clos_infos -> RedFlags.reds
val info_univs : clos_infos -> UGraph.t
val unfold_projection : clos_infos -> Names.Projection.t -> stack_member option
val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos
val push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos
val set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos
val info_relevances : clos_infos -> Sorts.relevance Range.t
val infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos
val norm_val : clos_infos -> clos_tab -> fconstr -> Constr.constr
val whd_val : clos_infos -> clos_tab -> fconstr -> Constr.constr
val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val eta_expand_ind_stack : Environ.env -> Names.inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack
val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit
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 kni : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val knr : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val zip : fconstr -> stack -> fconstr
val term_of_process : fconstr -> stack -> Constr.constr
val to_constr : Esubst.lift -> fconstr -> Constr.constr