@@ -1902,9 +1902,9 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1902 case find n imps [] of
1902 case find n imps [] of
1903 Just (tm, imps') ->
1903 Just (tm, imps') ->
1904 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1904 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1905− Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in
1905+ Nothing ->
1906− PImp p True l n ph :
1906+ PImp p True l n Placeholder :
1907− insImpAcc (M.insert n ph pnas) ps given imps
1907+ insImpAcc (M.insert n Placeholder pnas) ps given imps
1908 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1908 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1909 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1909 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
1910 case find n imps [] of
1910 case find n imps [] of