projects / darcs-mirror-agda-free-groups.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 1e83917)
Cleanup
authorJoachim Breitner <mail@joachim-breitner.de>
Mon, 7 May 2012 14:08:07 +0000 (14:08 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 7 May 2012 14:08:07 +0000 (14:08 +0000)
FreeGroups.agda patch | blob | history

diff --git a/FreeGroups.agda b/FreeGroups.agda
index 83363d1..6dce2b5 100644 (file)
--- a/FreeGroups.agda
+++ b/FreeGroups.agda
@@ -1,5 +1,4 @@
 open import Relation.Binary
-open import Level
 
 module FreeGroups {c ℓ} (S : Setoid c ℓ) where
 
Mirror of http://darcs.nomeata.de/agda-free-groups