coq 8.9.1 · OCaml Package

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

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

type 'a infos_cache

type 'a infos_tab

type !'a infos = {

i_flags : RedFlags.reds;
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 fterm =

| FRel of int
| FAtom of Constr.constr
| FCast of fconstr * Constr.cast_kind * fconstr
| 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 * Constr.constr) list * Constr.constr * fconstr Esubst.subs
| FProd of Names.Name.t * fconstr * fconstr
| FLetIn of Names.Name.t * fconstr * fconstr * Constr.constr * fconstr Esubst.subs
| FEvar of Constr.existential * fconstr Esubst.subs
| FLIFT of int * fconstr
| FCLOS of Constr.constr * fconstr Esubst.subs
| FLOCKED

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
| Zshift of int
| 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 -> Constr.constr) ->
  Constr.constr ->
  stack ->
  Constr.constr

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

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

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 norm_val : clos_infos -> fconstr infos_tab -> fconstr -> Constr.constr

val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> Constr.constr

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 : fconstr Esubst.subs -> Constr.constr -> fconstr

val mk_clos_vect : fconstr Esubst.subs -> Constr.constr array -> fconstr array

val kni : 
  clos_infos ->
  fconstr infos_tab ->
  fconstr ->
  stack ->
  fconstr * stack

val knr : 
  clos_infos ->
  fconstr infos_tab ->
  fconstr ->
  stack ->
  fconstr * stack

val kl : clos_infos -> fconstr infos_tab -> fconstr -> Constr.constr

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

package coq