(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function (** Precompute a VM value from a constr *) val val_of_constr : env -> constr -> Vmvalues.values