safe flags

agda · Sep 19, 2024 · 01fa420 · 01fa420
1 parent 54a2b1f
commit 01fa420
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Cubical/HITs/James/Stable.agda b/Cubical/HITs/James/Stable.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
 
 {-
   The stable version of the James splitting:

diff --git a/Cubical/HITs/Susp/SuspProduct.agda b/Cubical/HITs/Susp/SuspProduct.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
 
 {-
   The suspension of a Cartesian product is given by a triple wedge sum

diff --git a/Cubical/Homotopy/HiltonMilnor.agda b/Cubical/Homotopy/HiltonMilnor.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 {-
   The finitary Hilton–Milnor splitting