Module `Conversion`

type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
type 'a extended_conversion_function = ?⁠l2r:bool -> ?⁠reds:TransparentState.t -> Environ.env -> ?⁠evars:Constr.constr CClosure.evar_handler -> 'a -> 'a -> unit
type conv_pb = | CONV | CUMUL
type 'a universe_compare = { compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a; compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a; }
type 'a universe_state = 'a * 'a universe_compare
type 'b generic_conversion_function = 'b universe_state -> Constr.constr -> Constr.constr -> 'b
type 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraints.t

val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> Sorts.QUConstraints.t
val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
val sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
val convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
val checked_universes : UGraph.t universe_compare: This function never raise UnivInconsistency.

val conv : Constr.constr extended_conversion_function: These two functions can only raise NotConvertible

val conv_leq : Constr.types extended_conversion_function
val generic_conv : conv_pb -> l2r:bool -> TransparentState.t -> Environ.env -> ?⁠evars:Constr.constr CClosure.evar_handler -> 'a generic_conversion_function: Depending on the universe state functions, this might raise UniverseInconsistency in addition to NotConvertible (for better error messages).