package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cbv_infos
val shift_value : int -> cbv_value -> cbv_value
val stack_app : cbv_value array -> cbv_stack -> cbv_stack
val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
val apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr
val cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr