Skip to content

Commit e83814b

Browse files
authored
[ re #1465 ] Two more modules that are no longer --safe (#1498)
1 parent f2bd3aa commit e83814b

File tree

3 files changed

+4
-2
lines changed

3 files changed

+4
-2
lines changed

GenerateEverything.hs

+2
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,10 @@ sizedTypesModules = map modToFile
134134
, "Data.Container.Any"
135135
, "Data.Container.FreeMonad"
136136
, "Data.Nat.PseudoRandom.LCG.Unsafe"
137+
, "Data.Tree.Binary.Show"
137138
, "Data.Tree.Rose"
138139
, "Data.Tree.Rose.Properties"
140+
, "Data.Tree.Rose.Show"
139141
, "Data.Trie"
140142
, "Data.Trie.NonEmpty"
141143
, "Relation.Unary.Sized"

src/Data/Tree/Binary/Show.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
-- 1 dimensional pretty printing of binary trees
55
------------------------------------------------------------------------
66

7-
{-# OPTIONS --without-K --safe --sized-types #-}
7+
{-# OPTIONS --without-K --sized-types #-}
88

99
open import Level using (Level)
1010
open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_)

src/Data/Tree/Rose/Show.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
-- 1 dimensional pretty printing of rose trees
55
------------------------------------------------------------------------
66

7-
{-# OPTIONS --without-K --safe --sized-types #-}
7+
{-# OPTIONS --without-K --sized-types #-}
88

99
module Data.Tree.Rose.Show where
1010

0 commit comments

Comments
 (0)