Module `Nativenorm`

val native_norm : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types -> EConstr.constr
val native_infer_conv : ?⁠pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option: Conversion with inference of universe constraints