Skip to content

Commit 851001d

Browse files
committed
Add missing options pragma from ring quotient module
1 parent c15d31d commit 851001d

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/Algebra/Construct/Quotient/Ring.agda

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
-- Quotient rings
55
------------------------------------------------------------------------
66

7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
79
open import Algebra.Bundles using (Ring)
810
open import Algebra.Ideal using (Ideal)
911

0 commit comments

Comments
 (0)