Add missing flags

martinescardo · Aug 17, 2023 · c7cc8b1 · c7cc8b1
1 parent 5ffaaa3
commit c7cc8b1
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/source/Locales/PatchOfOmega.lagda b/source/Locales/PatchOfOmega.lagda
@@ -2,6 +2,8 @@ Ayberk Tosun, 17 August 2023.
 
 \begin{code}[hide]
 
+{-# OPTIONS --safe --without-K --exact-split #-}
+
 open import MLTT.Spartan
 open import UF.PropTrunc
 open import UF.FunExt