summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/Highlighting/Precise.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Interaction/Highlighting/Precise.hs')
-rw-r--r--src/full/Agda/Interaction/Highlighting/Precise.hs18
1 files changed, 9 insertions, 9 deletions
diff --git a/src/full/Agda/Interaction/Highlighting/Precise.hs b/src/full/Agda/Interaction/Highlighting/Precise.hs
index 932dafa..66f8f56 100644
--- a/src/full/Agda/Interaction/Highlighting/Precise.hs
+++ b/src/full/Agda/Interaction/Highlighting/Precise.hs
@@ -47,7 +47,7 @@ import Data.Map (Map)
import qualified Data.Map as Map
import Data.Typeable (Typeable)
-import qualified Agda.Syntax.Common as C
+import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete as SC
import Agda.Interaction.Highlighting.Range
@@ -72,16 +72,16 @@ data Aspect
-- | @NameKind@s are figured our during scope checking.
data NameKind
- = Bound -- ^ Bound variable.
- | Constructor C.Induction -- ^ Inductive or coinductive constructor.
+ = Bound -- ^ Bound variable.
+ | Constructor Common.Induction -- ^ Inductive or coinductive constructor.
| Datatype
- | Field -- ^ Record field.
+ | Field -- ^ Record field.
| Function
- | Module -- ^ Module name.
+ | Module -- ^ Module name.
| Postulate
- | Primitive -- ^ Primitive.
- | Record -- ^ Record type.
- | Argument -- ^ Named argument, like x in {x = v}
+ | Primitive -- ^ Primitive.
+ | Record -- ^ Record type.
+ | Argument -- ^ Named argument, like x in {x = v}
deriving (Eq, Show, Typeable)
-- | Other aspects, generated by type checking.
@@ -449,7 +449,7 @@ instance CoArbitrary File where
instance Arbitrary CompressedFile where
arbitrary = do
rs <- (\ns1 ns2 -> toRanges $ sort $
- ns1 ++ concatMap (\n -> [n, succ n]) ns2) <$>
+ ns1 ++ concatMap (\n -> [n, succ n]) (ns2 :: [Int])) <$>
arbitrary <*> arbitrary
CompressedFile <$> mapM (\r -> (,) r <$> arbitrary) rs
where