From 62230defc7b2ef27e40aafce8dd05d1e4ff09538 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Feb 2020 18:39:05 -0800
Subject: [PATCH] fix: `ppGoal` bug

---
 src/Init/Lean/Util/PPGoal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Util/PPGoal.lean b/src/Init/Lean/Util/PPGoal.lean
index bd1d058966..c264797706 100644
--- a/src/Init/Lean/Util/PPGoal.lean
+++ b/src/Init/Lean/Util/PPGoal.lean
@@ -21,7 +21,7 @@ match mctx.findDecl? mvarId with
     match ids, type? with
     | [], _        => fmt
     | _, none      => fmt
-    | _, some type => fmt ++ (Format.joinSep ids " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
+    | _, some type => fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
   let (varNames, type?, fmt) := mvarDecl.lctx.foldl
     (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
        let (varNames, prevType?, fmt) := acc;