@@ -437,10 +437,7 @@ process h fn (Check (PRef _ n))
437437 showMetavarInfo c imp ist n i
438438 = case lookupTy n (tt_ctxt ist) of
439439 (ty:_) -> putTy c imp ist i (delab ist ty)
440− putTy c imp ist 0 sc
441− = do ihputStrLn h $ "--------------------------------------"
442− ihputStrLn h $ showName (Just ist) [] False c n ++ " : "
443− ++ showImp (Just ist) imp c sc
440+ putTy c imp ist 0 sc = putGoal c imp ist sc
444441 putTy c imp ist i (PPi _ n t sc)
445442 = do ihputStrLn h $ " " ++
446443 (case n of
@@ -449,6 +446,11 @@ process h fn (Check (PRef _ n))
449446 _ -> showName (Just ist) [] False c n) ++
450447 " : " ++ showImp (Just ist) imp c t
451448 putTy c imp ist (i-1) sc
449+ putTy c imp ist _ sc = putGoal c imp ist sc
450+ putGoal c imp ist g
451+ = do ihputStrLn h $ "--------------------------------------"
452+ ihputStrLn h $ showName (Just ist) [] False c n ++ " : "
453+ ++ showImp (Just ist) imp c g
452454
453455
454456process h fn (Check t)