removed cubical flags

Freek98 · Freek98 · commit 3954418b4a7c · 2025-08-13T17:48:57.000+02:00
diff --git a/Cubical/Data/Nat/Bijections/FinN.agda b/Cubical/Data/Nat/Bijections/FinN.agda
@@ -1,4 +1,3 @@
-{-# OPTIONS --cubical #-}
 module Cubical.Data.Nat.Bijections.FinN where
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Data/Nat/Bijections/IncreasingFunction.agda b/Cubical/Data/Nat/Bijections/IncreasingFunction.agda
@@ -1,4 +1,3 @@
-{-# OPTIONS --cubical #-}
 module Cubical.Data.Nat.Bijections.IncreasingFunction where
 
 {- Consider an increasing function f : ℕ → ℕ with f 0 ≡ 0.
diff --git a/Cubical/Data/Nat/Bijections/Product.agda b/Cubical/Data/Nat/Bijections/Product.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --cubical #-}
-
 module Cubical.Data.Nat.Bijections.Product where
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Data/Nat/Bijections/Sum.agda b/Cubical/Data/Nat/Bijections/Sum.agda
@@ -1,4 +1,3 @@
-{-# OPTIONS --cubical #-}
 module Cubical.Data.Nat.Bijections.Sum where
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Data/Nat/MoreOrderProperties.agda b/Cubical/Data/Nat/MoreOrderProperties.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --cubical #-}
-
 module Cubical.Data.Nat.MoreOrderProperties where
 
 open import Cubical.Foundations.Prelude

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-{-# OPTIONS --cubical #-}`
`2`	`1`	`module Cubical.Data.Nat.Bijections.FinN where`
`3`	`2`
`4`	`3`	`open import Cubical.Foundations.Prelude`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-{-# OPTIONS --cubical #-}`
`2`	`1`	`module Cubical.Data.Nat.Bijections.IncreasingFunction where`
`3`	`2`
`4`	`3`	`{- Consider an increasing function f : ℕ → ℕ with f 0 ≡ 0.`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-{-# OPTIONS --cubical #-}`
`2`		`-`
`3`	`1`	`module Cubical.Data.Nat.Bijections.Product where`
`4`	`2`
`5`	`3`	`open import Cubical.Foundations.Prelude`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-{-# OPTIONS --cubical #-}`
`2`	`1`	`module Cubical.Data.Nat.Bijections.Sum where`
`3`	`2`
`4`	`3`	`open import Cubical.Foundations.Prelude`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-{-# OPTIONS --cubical #-}`
`2`		`-`
`3`	`1`	`module Cubical.Data.Nat.MoreOrderProperties where`
`4`	`2`
`5`	`3`	`open import Cubical.Foundations.Prelude`