@@ -437,10 +437,7 @@ process h fn (Check (PRef _ n))
437 showMetavarInfo c imp ist n i
437 showMetavarInfo c imp ist n i
438 = case lookupTy n (tt_ctxt ist) of
438 = case lookupTy n (tt_ctxt ist) of
439 (ty:_) -> putTy c imp ist i (delab ist ty)
439 (ty:_) -> putTy c imp ist i (delab ist ty)
440− putTy c imp ist 0 sc
440+ putTy c imp ist 0 sc = putGoal c imp ist sc
441− = do ihputStrLn h $ "--------------------------------------"
442− ihputStrLn h $ showName (Just ist) [] False c n ++ " : "
443− ++ showImp (Just ist) imp c sc
444 putTy c imp ist i (PPi _ n t sc)
441 putTy c imp ist i (PPi _ n t sc)
445 = do ihputStrLn h $ " " ++
442 = do ihputStrLn h $ " " ++
446 (case n of
443 (case n of
@@ -449,6 +446,11 @@ process h fn (Check (PRef _ n))
449 _ -> showName (Just ist) [] False c n) ++
446 _ -> showName (Just ist) [] False c n) ++
450 " : " ++ showImp (Just ist) imp c t
447 " : " ++ showImp (Just ist) imp c t
451 putTy c imp ist (i-1) sc
448 putTy c imp ist (i-1) sc
449+ putTy c imp ist _ sc = putGoal c imp ist sc
451+ = do ihputStrLn h $ "--------------------------------------"
452+ ihputStrLn h $ showName (Just ist) [] False c n ++ " : "
453+ ++ showImp (Just ist) imp c g
454process h fn (Check t)
456process h fn (Check t)