Module Conversion

exception NotConvertible
type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars: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.

These two functions can only raise NotConvertible

val generic_conv : conv_pb -> l2r:bool -> TransparentState.t -> Environ.env -> ?evars: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).