drop unused import
authorHelmut Grohne <helmut@subdivi.de>
Mon, 10 Dec 2012 11:48:25 +0000 (12:48 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Mon, 10 Dec 2012 11:48:25 +0000 (12:48 +0100)
Bidir.agda

index 3902a06..bed902a 100644 (file)
@@ -16,7 +16,6 @@ open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Data.Empty using (⊥-elim)
 open import Function using (id ; _∘_ ; flip)
 open import Relation.Nullary using (yes ; no)
-open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core using (refl)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; _≗_ ; trans)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)