From 22af0e085f03eb5e60d82d1211c09a7e5706bae4 Mon Sep 17 00:00:00 2001
From: Trebor-Huang <treborhuang@foxmail.com>
Date: Thu, 19 Sep 2024 22:16:54 +0800
Subject: [PATCH] safe flags

---
 Cubical/HITs/James/Stable.agda     | 2 +-
 Cubical/Homotopy/HiltonMilnor.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/HITs/James/Stable.agda b/Cubical/HITs/James/Stable.agda
index 7c9915f49..48e6af5b7 100644
--- 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/Homotopy/HiltonMilnor.agda b/Cubical/Homotopy/HiltonMilnor.agda
index c8f967ac0..425a5e797 100644
--- 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