CbvSourceEntry point for cbv normalization of a constr
type cbv_value = | VAL of int * Constr.constr| STACK of int * cbv_value * cbv_stack| CBN of Constr.constr * cbv_value Esubst.subs| LAM of int
* (Names.Name.t Context.binder_annot * Constr.constr) list
* Constr.constr
* cbv_value Esubst.subs| FIXP of Constr.fixpoint * cbv_value Esubst.subs * cbv_value array| COFIXP of Constr.cofixpoint * cbv_value Esubst.subs * cbv_value array| CONSTR of Names.constructor Univ.puniverses * cbv_value array| PRIMITIVE of CPrimitives.t * Constr.pconstant * cbv_value array| ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_valueand cbv_stack = | TOP| APP of cbv_value array * cbv_stack| CASE of Univ.Instance.t
* Constr.constr array
* Constr.case_return
* Constr.case_branch array
* Constr.case_invert
* Constr.case_info
* cbv_value Esubst.subs
* cbv_stack| PROJ of Names.Projection.t * cbv_stackval cbv_stack_term :
cbv_infos ->
cbv_stack ->
cbv_value Esubst.subs ->
Constr.constr ->
cbv_valuerecursive functions...
val norm_head :
cbv_infos ->
cbv_value Esubst.subs ->
Constr.constr ->
cbv_stack ->
cbv_value * cbv_stackEnd of cbv debug section i