Unused pragma

yveshauser · yveshauser · commit c00e03be1524 · 2025-04-10T11:20:00.000+02:00
diff --git a/formal-spec/Leios/Foreign/Types.agda b/formal-spec/Leios/Foreign/Types.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
 open import Data.Char.Base as C using (Char)
 import Data.String as S
 open import Data.Integer using (+_; ∣_∣)

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-{-# OPTIONS --allow-unsolved-metas #-}`
`2`		`-`
`3`	`1`	`open import Data.Char.Base as C using (Char)`
`4`	`2`	`import Data.String as S`
`5`	`3`	`open import Data.Integer using (+_; ∣_∣)`