@@ -8,6 +8,7 @@ import Idris.REPLParser
88import Idris.ElabDecls
99import Idris.ElabTerm
1010import Idris.Error
11+import Idris.ErrReverse
1112import Idris.Delaborate
1213import Idris.Prover
1314import Idris.Parser
@@ -486,7 +487,7 @@ process h fn (Check (PRef _ n))
486487 where
487488 showMetavarInfo imp ist n i
488489 = case lookupTy n (tt_ctxt ist) of
489− (ty:_) -> putTy imp ist i [] (delab ist ty)
490+ (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
490491 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
491492 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
492493 putTy imp ist i bnd (PPi _ n t sc)