Skip to content

Commit b2542e3

Browse files
GulinSSspcfox
andcommitted
ScopedSnocList: Fix CI
Co-authored-by: Viktor Yudov <[email protected]>
1 parent 7fc2f3a commit b2542e3

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

Diff for: src/Compiler/CompileExpr.idr

+2-2
Original file line numberDiff line numberDiff line change
@@ -478,7 +478,7 @@ mutual
478478
-- the RHS
479479
then do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"
480480

481-
sc' : CExp (vars <>< args) <- toCExpTree n sc
481+
sc' <- toCExpTree n sc
482482
let sc'' : CExp (vars ++ cast args)
483483
:= rewrite sym $ fishAsSnocAppend vars args in sc'
484484

@@ -493,7 +493,7 @@ mutual
493493
let (s, env) : (_, SubstCEnv (cast args) (vars :< MN "eff" 0))
494494
= mkSubst 0 (CLocal fc First) pos args
495495
496-
sc' : CExp (vars <>< args) <- toCExpTree n sc
496+
sc' <- toCExpTree n sc
497497

498498
let sc'' : CExp (vars ++ cast args)
499499
:= rewrite sym $ fishAsSnocAppend vars args in sc'

Diff for: src/Core/Name/Scoped.idr

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import Core.Name
44
import Core.Name.CompatibleVars
55

66
import Data.SnocList
7-
import Data.SnocList.HasLength
7+
import Libraries.Data.SnocList.HasLength
88
import Libraries.Data.SnocList.SizeOf
99
import Libraries.Data.List.SizeOf
1010

0 commit comments

Comments
 (0)