Module Vconv

val vm_conv : Reduction.conv_pb -> Constr.types Reduction.kernel_conversion_function
val vm_conv_gen : Reduction.conv_pb -> (Constr.existential -> Constr.constr option) -> (Constr.types'a) Reduction.generic_conversion_function

A conversion function parametrized by a universe comparator and evar normalizer. Used outside of the kernel.