NativeconvSourceThis module implements the conversion test by compiling to OCaml code
val native_conv :
Conversion.conv_pb ->
Genlambda.evars ->
Constr.types Conversion.kernel_conversion_functionval native_conv_gen :
Conversion.conv_pb ->
Genlambda.evars ->
Environ.env ->
('a, 'err) Conversion.generic_conversion_functionA conversion function parametrized by a universe comparator. Used outside of the kernel.