summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/MetaVars/Mention.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/MetaVars/Mention.hs')
-rw-r--r--src/full/Agda/TypeChecking/MetaVars/Mention.hs3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/full/Agda/TypeChecking/MetaVars/Mention.hs b/src/full/Agda/TypeChecking/MetaVars/Mention.hs
index 4a02019..36c960e 100644
--- a/src/full/Agda/TypeChecking/MetaVars/Mention.hs
+++ b/src/full/Agda/TypeChecking/MetaVars/Mention.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
module Agda.TypeChecking.MetaVars.Mention where
@@ -15,7 +14,7 @@ instance MentionsMeta Term where
Lam _ b -> mm b
Lit{} -> False
Def _ args -> mm args
- Con _ args -> mm args
+ Con _ _ args -> mm args
Pi a b -> mm (a, b)
Sort s -> mm s
Level l -> mm l