coq 8.10.2 · OCaml Package

coq

val stats : bool ref

val with_stats : 'a Lazy.t -> 'a

module type RedFlagsSig = sig ... end

module RedFlags : RedFlagsSig

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

val unfold_red : Names.evaluable_global_reference -> RedFlags.reds

type table_key = Names.Constant.t Univ.puniverses Names.tableKey

module KeyTable : sig ... end

type fconstr

type fterm =

| FRel of int
| FAtom of Constr.constr
| FFlex of table_key
| FInd of Names.inductive Univ.puniverses
| FConstruct of Names.constructor Univ.puniverses
| FApp of fconstr * fconstr array
| FProj of Names.Projection.t * fconstr
| FFix of Constr.fixpoint * fconstr Esubst.subs
| FCoFix of Constr.cofixpoint * fconstr Esubst.subs
| FCaseT of Constr.case_info * Constr.constr * fconstr * Constr.constr array * fconstr Esubst.subs
| FLambda of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * fconstr Esubst.subs
| FProd of Names.Name.t Context.binder_annot * fconstr * Constr.constr * fconstr Esubst.subs
| FLetIn of Names.Name.t Context.binder_annot * fconstr * fconstr * Constr.constr * fconstr Esubst.subs
| FEvar of Constr.existential * fconstr Esubst.subs
| FInt of Uint63.t
| FLIFT of int * fconstr
| FCLOS of Constr.constr * fconstr Esubst.subs
| FLOCKED

type !'a next_native_args = (CPrimitives.arg_kind * 'a) list

type stack_member =

| Zapp of fconstr array
| ZcaseT of Constr.case_info * Constr.constr * Constr.constr array * fconstr Esubst.subs
| Zproj of Names.Projection.Repr.t
| Zfix of fconstr * stack
| Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
| Zshift of int
| 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 get_native_args1 : 
  CPrimitives.t ->
  Constr.pconstant ->
  stack ->
  fconstr list * fconstr * fconstr next_native_args * stack

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

val destFLambda : 
  (fconstr Esubst.subs -> Constr.constr -> fconstr) ->
  fconstr ->
  Names.Name.t Context.binder_annot * fconstr * fconstr

type optrel =

| Unknown
| KnownR
| KnownI

val relevance_of : fconstr -> optrel

val set_relevance : Sorts.relevance -> fconstr -> unit

type clos_infos

type clos_tab

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 create_tab : unit -> clos_tab

val info_env : clos_infos -> Environ.env

val info_flags : clos_infos -> RedFlags.reds

val unfold_projection : clos_infos -> Names.Projection.t -> stack_member option

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 unfold_reference : 
  clos_infos ->
  clos_tab ->
  table_key ->
  fconstr Declarations.constant_def

val lift_fconstr : int -> fconstr -> fconstr

val lift_fconstr_vect : int -> fconstr array -> fconstr array

val mk_clos : fconstr Esubst.subs -> Constr.constr -> fconstr

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 kl : clos_infos -> clos_tab -> fconstr -> Constr.constr

val to_constr : Esubst.lift -> fconstr -> Constr.constr

package coq