package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cbv_infos

Entry point for cbv normalization of a constr

val shift_value : int -> cbv_value -> cbv_value
val stack_app : cbv_value list -> cbv_stack -> cbv_stack
val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack

recursive functions...

val apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr
val cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr

End of cbv debug section i