package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

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