@@ -100,11 +100,14 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
100 | n == eqTy = PEq un (de env [] l) (de env [] r)
100 | n == eqTy = PEq un (de env [] l) (de env [] r)
101 | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder
101 | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder
102 (de env [] r)
102 (de env [] r)
103− deFn env (P _ n _) args | not mvs
103+ deFn env f@(P _ n _) args
104+ | n `elem` map snd env
105+ = PApp un (de env [] f) (map pexp (map (de env []) args))
106+ deFn env (P _ n _) args
104− = case lookup n (idris_metavars ist) of
107+ | not mvs = case lookup n (idris_metavars ist) of
105− Just (Just _, mi, _) ->
108+ Just (Just _, mi, _) ->
106− mkMVApp n (drop mi (map (de env []) args))
109+ mkMVApp n (drop mi (map (de env []) args))
107− _ -> mkPApp n (map (de env []) args)
110+ _ -> mkPApp n (map (de env []) args)
108 | otherwise = mkPApp n (map (de env []) args)
111 | otherwise = mkPApp n (map (de env []) args)
109 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
112 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
@@ -113,7 +116,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
113 mkMVApp n args
116 mkMVApp n args
114 = PApp un (PMetavar n) (map pexp args)
117 = PApp un (PMetavar n) (map pexp args)
115 mkPApp n args
118 mkPApp n args
116− | [imps] <- lookupCtxt n (idris_implicits ist)
119+ | Just imps <- lookupCtxtExact n (idris_implicits ist)
117 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
120 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
118 | otherwise = PApp un (PRef un n) (map pexp args)
121 | otherwise = PApp un (PRef un n) (map pexp args)