package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

Sourcetype cbv_infos

Entry point for cbv normalization of a constr

val create_cbv_infos : 
  CClosure.RedFlags.reds ->
  Environ.env ->
  Evd.evar_map ->
  cbv_infos

Sourceval cbv_norm : cbv_infos -> EConstr.constr -> EConstr.constr

Sourcetype cbv_value =

Sourceand cbv_stack =

Sourceval shift_value : int -> cbv_value -> cbv_value

Sourceval stack_app : cbv_value array -> cbv_stack -> cbv_stack

Sourceval strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack

val cbv_stack_term : 
  cbv_infos ->
  cbv_stack ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  cbv_value

recursive functions...

val cbv_norm_term : 
  cbv_infos ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  Constr.constr

val norm_head : 
  cbv_infos ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  cbv_stack ->
  cbv_value * cbv_stack

Sourceval apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr

Sourceval cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr

End of cbv debug section i