From 249c87859756a0561863644c374b7e2f8750d4dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Aug 2014 15:21:23 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): warning message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 151c90c85..be597a0d0 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1279,12 +1279,14 @@ public:
 
     void display_flyinfo(substitution const & s) {
         instantiate_flyinfo(s);
-        optional<flyinfo_data> prev;
+        flyinfo_data prev;
+        bool first = true;
         for (auto const & p : m_flyinfo_data) {
-            if (!prev || p.first != prev->first) {
+            if (first || p.first != prev.first) {
                 display_flyinfo_data(p);
                 prev = p;
             }
+            first = false;
         }
     }