Library Coq.Init.Prelude

Require Export Notations.
Require Export Logic.
Require Export Logic_Type.
Require Export Datatypes.
Require Export Specif.
Require Coq.Init.Decimal.
Require Coq.Init.Nat.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
Require Export Coq.Init.Tauto.
Declare ML Module "cc_plugin".
Declare ML Module "ground_plugin".
Declare ML Module "numeral_notation_plugin".

Arguments Nat.of_uint d%dec_uint_scope.
Arguments Nat.of_int d%dec_int_scope.
Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
  : dec_uint_scope.
Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
  : dec_int_scope.

Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).

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