Library Corelib.Init.Prelude

Require Export Notations.
Require Export Equality.
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.


Export
  Number.NumberNotations
  Nat.NumberNotations
  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.