Library Coq.Init.Prelude

Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
Add Search Blacklist "_admitted" "_subproof" "Private_".