summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/SearchAbout.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Interaction/SearchAbout.hs')
-rw-r--r--src/full/Agda/Interaction/SearchAbout.hs6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/full/Agda/Interaction/SearchAbout.hs b/src/full/Agda/Interaction/SearchAbout.hs
index 9a73a27..0f489ce 100644
--- a/src/full/Agda/Interaction/SearchAbout.hs
+++ b/src/full/Agda/Interaction/SearchAbout.hs
@@ -28,7 +28,7 @@ collectNamesInTerm :: Term -> [A.QName]
collectNamesInTerm (Var _ els) = collectNamesInElims els
collectNamesInTerm (Lam ty t) = collectNamesInTerm $ unAbs t
collectNamesInTerm (Def n els) = n : collectNamesInElims els
-collectNamesInTerm (Con n args) = conName n : collectNamesInArgs args
+collectNamesInTerm (Con n _ args) = conName n : collectNamesInArgs args
collectNamesInTerm (Pi dom cod) = collectNamesInType (Com.unDom dom) ++ collectNamesInType (unAbs cod)
collectNamesInTerm (Shared t) = collectNamesInTerm $ ignoreSharing $ derefPtr t
collectNamesInTerm _ = []
@@ -38,7 +38,7 @@ collectNamesInElims = concatMap collectNamesInElim
collectNamesInElim :: Elim -> [A.QName]
collectNamesInElim (Apply a) = collectNamesInTerm $ Com.unArg a
-collectNamesInElim (Proj n) = [n]
+collectNamesInElim (Proj _ n)= [n]
collectNamesInArgs :: Args -> [A.QName]
collectNamesInArgs = concatMap (collectNamesInTerm . Com.unArg)
@@ -68,7 +68,7 @@ findMentions norm rg nm = do
| otherwise = Right str
anames (DefinedName _ an) = [an]
- anames (FieldName an) = [an]
+ anames (FieldName ans) = ans
anames (ConstructorName ans) = ans
anames (PatternSynResName an) = [an]
anames _ = []