Module ConversionSource

Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> (unit, unit) result
Sourcetype 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> 'a -> 'a -> (unit, unit) result
Sourcetype conv_pb =
  1. | CONV
  2. | CUMUL
Sourcetype ('a, 'err) universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
  2. compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
  3. compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
}
Sourcetype ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
Sourcetype ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> Constr.constr -> Constr.constr -> ('a, 'err option) result
Sourceval get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> Sorts.QUConstraints.t
Sourceval inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
Sourceval constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
Sourceval sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) result * ('a, 'err) universe_compare
Sourceval convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) result * ('a, 'err) universe_compare
Sourceval checked_universes : (UGraph.t, 'err) universe_compare

This function never returns an non-empty error.

These two functions can only fail with unit

Sourceval 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).