Module Conversion

type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> (unit, unit) Stdlib.result
type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> 'a -> 'a -> (unit, unit) Stdlib.result
type conv_pb =
| CONV
| CUMUL
type ('a, 'err) universe_compare = {
compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) Stdlib.result;
compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) Stdlib.result;
compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) Stdlib.result;
}
type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> Constr.constr -> Constr.constr -> ('a, 'err option) Stdlib.result
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, 'err) universe_compare) -> ('a, 'err option) Stdlib.result * ('a, 'err) universe_compare
val convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) Stdlib.result * ('a, 'err) universe_compare
val checked_universes : (UGraph.t, 'err) universe_compare

This function never returns an non-empty error.

These two functions can only fail with unit

val generic_conv : conv_pb -> l2r:bool -> TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> ('a, 'err) generic_conversion_function

The failure values depend on the universe state functions (for better error messages).