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.Numeral
.
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_".