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 Constr.evar_handler ->
'a ->
'a ->
unit
type 'a universe_compare = {
compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; |
compare_instances : flex:bool ->
Univ.Instance.t ->
Univ.Instance.t ->
'a ->
'a; |
compare_cumul_instances : conv_pb ->
Univ.Variance.t array ->
Univ.Instance.t ->
Univ.Instance.t ->
'a ->
'a; |
}
type 'a universe_state = 'a * 'a universe_compare
type ('a, 'b) generic_conversion_function =
Environ.env ->
'b universe_state ->
'a ->
'a ->
'b
type 'a infer_conversion_function =
Environ.env ->
'a ->
'a ->
Univ.Constraints.t
val get_cumulativity_constraints :
conv_pb ->
Univ.Variance.t array ->
Univ.Instance.t ->
Univ.Instance.t ->
Univ.Constraints.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 ->
Univ.Instance.t ->
Univ.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 ->
Constr.constr Constr.evar_handler ->
TransparentState.t ->
( Constr.constr, 'a ) generic_conversion_function
Depending on the universe state functions, this might raise UniverseInconsistency
in addition to NotConvertible
(for better error messages).
val default_conv : conv_pb -> Constr.types kernel_conversion_function
val default_conv_leq : Constr.types kernel_conversion_function