Ensure all modules are compiled without K.

pcapriotti · pcapriotti · commit f9728db328a4 · 2013-02-28T20:40:12.000Z
diff --git a/decidable.agda b/decidable.agda
@@ -1,4 +1,3 @@
-
 {-# OPTIONS --without-K  #-}
 
 module decidable where
diff --git a/function/extensionality/dependent.agda b/function/extensionality/dependent.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K #-}
 module function.extensionality.dependent where
 
 open import level using (_⊔_; ↑; lift)
diff --git a/sets.agda b/sets.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K #-}
 module sets where
 
 open import sets.bool  public renaming (_≟_ to _≟B_)
diff --git a/sets/bool.agda b/sets/bool.agda
@@ -1,4 +1,3 @@
-
 {-# OPTIONS --without-K  #-}
 
 module sets.bool where
diff --git a/sets/nat.agda b/sets/nat.agda
@@ -1,4 +1,3 @@
-
 {-# OPTIONS --without-K  #-}
 
 module sets.nat where
diff --git a/sets/unit.agda b/sets/unit.agda
@@ -1,4 +1,3 @@
-
 {-# OPTIONS --without-K  #-}
 
 module sets.unit where

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --without-K #-}`
`1`	`2`	`module function.extensionality.dependent where`
`2`	`3`
`3`	`4`	`open import level using (_⊔_; ↑; lift)`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --without-K #-}`
`1`	`2`	`module sets where`
`2`	`3`
`3`	`4`	`open import sets.bool public renaming (_≟_ to _≟B_)`