@@ -241,7 +241,7 @@ elab ist info pattern tcgen fn tm
241 let fty = fnTy argTys rty
241 let fty = fnTy argTys rty
242-- trace (show (ptm, map fst argTys)) $ focus fn
242-- trace (show (ptm, map fst argTys)) $ focus fn
243 -- build and defer the function application
243 -- build and defer the function application
244− attack; deferType f fty (map fst argTys); solve
244+ attack; deferType (mkN f) fty (map fst argTys); solve
245 -- elaborate the arguments, to unify their types. They all have to
245 -- elaborate the arguments, to unify their types. They all have to
246 -- be explicit.
246 -- be explicit.
247 mapM_ elabIArg (zip argTys args)
247 mapM_ elabIArg (zip argTys args)
@@ -261,6 +261,11 @@ elab ist info pattern tcgen fn tm
262 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
262 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
263 elabIArg _ = return () -- already done, just a name
263 elabIArg _ = return () -- already done, just a name
266+ mkN n = case namespace info of
267+ Just xs@(_:_) -> NS n xs
265 elab' (ina, g) tm@(PApp fc (PRef _ f) args')
270 elab' (ina, g) tm@(PApp fc (PRef _ f) args')
266 = do let args = {- case lookupCtxt f (inblock info) of
271 = do let args = {- case lookupCtxt f (inblock info) of