summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Internal/Defs.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Internal/Defs.hs')
-rw-r--r--src/full/Agda/Syntax/Internal/Defs.hs8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/full/Agda/Syntax/Internal/Defs.hs b/src/full/Agda/Syntax/Internal/Defs.hs
index dd4fc38..a79b7be 100644
--- a/src/full/Agda/Syntax/Internal/Defs.hs
+++ b/src/full/Agda/Syntax/Internal/Defs.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
-- | Extract used definitions from terms.
module Agda.Syntax.Internal.Defs where
@@ -82,6 +81,7 @@ instance GetDefs Sort where
Type l -> getDefs l
Prop -> return ()
Inf -> return ()
+ SizeUniv -> return ()
DLub s s' -> getDefs s >> getDefs s'
instance GetDefs Level where
@@ -95,7 +95,7 @@ instance GetDefs LevelAtom where
getDefs a = case a of
MetaLevel x vs -> getDefs x >> getDefs vs
BlockedLevel _ v -> getDefs v
- NeutralLevel v -> getDefs v
+ NeutralLevel _ v -> getDefs v
UnreducedLevel v -> getDefs v
-- collection instances