Conversion (coq-core.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:Constr.constr Constr.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 ->
  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