Skip to content

Commit 9427d94

Browse files
felixwellenfelixwellen
committed
add --safe to the library flags and remove the option everywhere
by now, --safe is compatible with --guardedness, so we can just add --safe to the library flags
1 parent 1d78137 commit 9427d94

File tree

1,091 files changed

+249
-1091
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,091 files changed

+249
-1091
lines changed

‎Cubical/Algebra/AbGroup.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup where
32

43
open import Cubical.Algebra.AbGroup.Base public

‎Cubical/Algebra/AbGroup/Base.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Base where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DiffInt.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
-- It is recommended to use Cubical.Algebra.CommRing.Instances.Int
22
-- instead of this file.
33

4-
{-# OPTIONS --safe #-}
54
module Cubical.Algebra.AbGroup.Instances.DiffInt where
65

76
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DirectProduct.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectProduct where
32

43
open import Cubical.Data.Sigma

‎Cubical/Algebra/AbGroup/Instances/DirectSumFun.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectSumFun where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DirectSumHIT.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectSumHIT where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# OPTIONS --safe --lossy-unification #-}
1+
{-# OPTIONS --lossy-unification #-}
22
module Cubical.Algebra.AbGroup.Instances.FreeAbGroup where
33

44
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/Hom.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
-- In other words, Ab is cartesian closed.
55
-- This is needed to show Ab is an abelian category.
66

7-
{-# OPTIONS --safe #-}
87

98
module Cubical.Algebra.AbGroup.Instances.Hom where
109

‎Cubical/Algebra/AbGroup/Instances/Int.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.Int where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/IntMod.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.IntMod where
32

43
open import Cubical.Foundations.Prelude

0 commit comments

Comments
 (0)