Library Coq.Init.Prelude

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

Arguments Nat.of_hex_uint d%hex_uint_scope.
Arguments Nat.of_hex_int d%hex_int_scope.

Arguments Nat.of_uint d%dec_uint_scope.
Arguments Nat.of_int d%dec_int_scope.


Export Byte.ByteSyntaxNotations.

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