package coq

You can search for identifiers within the package.

in-package search v0.2.0

package coq

Legend:
Library
Module
Module type
Parameter
Class
Class type

val stats : bool Stdlib.ref

val with_stats : 'a Stdlib.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

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

module KeyTable : sig ... end

type fconstr

type finvert

type fterm =

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

type stack_member =

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 : 
  ?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 unfold_reference : 
  clos_infos ->
  clos_tab ->
  table_key ->
  (fconstr, Util.Empty.t) Declarations.constant_def

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 : 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 zip : fconstr -> stack -> fconstr

val term_of_process : fconstr -> stack -> Constr.constr

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