summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Level.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Level.hs')
-rw-r--r--src/full/Agda/TypeChecking/Level.hs6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/full/Agda/TypeChecking/Level.hs b/src/full/Agda/TypeChecking/Level.hs
index dc934a2..fa1baa0 100644
--- a/src/full/Agda/TypeChecking/Level.hs
+++ b/src/full/Agda/TypeChecking/Level.hs
@@ -145,9 +145,9 @@ levelView' a = do
mkAtom a = do
b <- reduceB' a
return $ case ignoreSharing <$> b of
- NotBlocked (MetaV m as) -> atom $ MetaLevel m as
- NotBlocked _ -> atom $ NeutralLevel (ignoreBlocking b)
- Blocked m _ -> atom $ BlockedLevel m (ignoreBlocking b)
+ NotBlocked _ (MetaV m as) -> atom $ MetaLevel m as
+ NotBlocked r _ -> atom $ NeutralLevel r $ ignoreBlocking b
+ Blocked m _ -> atom $ BlockedLevel m $ ignoreBlocking b
atom a = Max [Plus 0 a]