Module `Nativeconv`

This module implements the conversion test by compiling to OCaml code

val native_conv : Reduction.conv_pb -> Nativelambda.evars -> Constr.types Reduction.kernel_conversion_function
val native_conv_gen : Reduction.conv_pb -> Nativelambda.evars -> (Constr.types, 'a) Reduction.generic_conversion_function: A conversion function parametrized by a universe comparator. Used outside of the kernel.