coq 8.7.2 · OCaml Package

coq

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

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 Term.puniverses Names.tableKey

type 'a infos_cache

type !'a infos = {

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

| FRel of int
| FAtom of Term.constr
| FCast of fconstr * Term.cast_kind * fconstr
| FFlex of table_key
| FInd of Names.inductive Term.puniverses
| FConstruct of Names.constructor Term.puniverses
| FApp of fconstr * fconstr array
| FProj of Names.projection * fconstr
| FFix of Term.fixpoint * fconstr Esubst.subs
| FCoFix of Term.cofixpoint * fconstr Esubst.subs
| FCaseT of Term.case_info * Term.constr * fconstr * Term.constr array * fconstr Esubst.subs
| FLambda of int * (Names.Name.t * Term.constr) list * Term.constr * fconstr Esubst.subs
| FProd of Names.Name.t * fconstr * fconstr
| FLetIn of Names.Name.t * fconstr * fconstr * Term.constr * fconstr Esubst.subs
| FEvar of Term.existential * fconstr Esubst.subs
| FLIFT of int * fconstr
| FCLOS of Term.constr * fconstr Esubst.subs
| FLOCKED

type stack_member =

| Zapp of fconstr array
| ZcaseT of Term.case_info * Term.constr * Term.constr array * fconstr Esubst.subs
| Zproj of int * int * Names.constant
| 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 -> 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

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

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

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

val mk_clos_deep : 
  (fconstr Esubst.subs -> Term.constr -> fconstr) ->
  fconstr Esubst.subs ->
  Term.constr ->
  fconstr

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

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

val kl : clos_infos -> fconstr -> Term.constr

val to_constr : 
  (Esubst.lift -> fconstr -> Term.constr) ->
  Esubst.lift ->
  fconstr ->
  Term.constr

package coq