Module `Nativenorm`

This module implements normalization by evaluation to OCaml code

val get_profile_filename : unit -> string
val set_profile_filename : string -> unit
val get_profiling_enabled : unit -> bool
val set_profiling_enabled : bool -> unit
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