Library Corelib.Init.Prelude

Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Corelib.Init.Byte.
Require Corelib.Init.Decimal.
Require Corelib.Init.Hexadecimal.
Require Corelib.Init.Number.
Require Corelib.Init.Nat.
Require Export Peano.
Require Export Corelib.Init.Wf.
Require Export Corelib.Init.Ltac.
Require Export Corelib.Init.Tactics.
Require Export Corelib.Init.Tauto.
Require Export Corelib.Init.Sumbool.

Arguments Nat.of_hex_uint d%_hex_uint_scope.
Arguments Nat.of_hex_int d%_hex_int_scope.
Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
  : hex_uint_scope.
Number Notation Number.int Number.int_of_int Number.int_of_int
  : hex_int_scope.

Arguments Nat.of_uint d%_dec_uint_scope.
Arguments Nat.of_int d%_dec_int_scope.
Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
  : dec_uint_scope.
Number Notation Number.int Number.int_of_int Number.int_of_int
  : dec_int_scope.

Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint (abstract after 5000) : hex_nat_scope.
Number Notation nat Nat.of_num_uint Nat.to_num_uint (abstract after 5000) : nat_scope.

Export Byte.ByteSyntaxNotations.

Add Search Blacklist "_subproof" "_subterm" "Private_".

#[universes(polymorphic=yes)] Definition ReverseCoercionSource (T : Type) := T.
#[universes(polymorphic=yes)] Definition ReverseCoercionTarget (T : Type) := T.
#[warning="-uniform-inheritance", reversible=no, universes(polymorphic=yes)]
Coercion reverse_coercion {T' T} (x' : T') (x : ReverseCoercionSource T)
  : ReverseCoercionTarget T' := x'.
Register reverse_coercion as core.coercion.reverse_coercion.