@@ -8,6 +8,7 @@ import Idris.REPLParser
8import Idris.ElabDecls
8import Idris.ElabDecls
9import Idris.ElabTerm
9import Idris.ElabTerm
10import Idris.Error
10import Idris.Error
11+import Idris.ErrReverse
11import Idris.Delaborate
12import Idris.Delaborate
12import Idris.Prover
13import Idris.Prover
13import Idris.Parser
14import Idris.Parser
@@ -486,7 +487,7 @@ process h fn (Check (PRef _ n))
487 showMetavarInfo imp ist n i
488 showMetavarInfo imp ist n i
488 = case lookupTy n (tt_ctxt ist) of
489 = 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))
490 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
491 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
491 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
492 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
492 putTy imp ist i bnd (PPi _ n t sc)
493 putTy imp ist i bnd (PPi _ n t sc)