From 100b3abf1d6f1dd5b09f86948c8bfde3342102c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Oct 2014 10:48:41 -0700
Subject: [PATCH] fix(frontends/lean/pp): bug in notation matching procedure

---
 src/frontends/lean/pp.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f6c9a03a9..f60f99aaf 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -609,9 +609,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
         return true;
     } else if (is_placeholder(p)) {
         return true;
-    } else if (is_constant(p)) {
-        if (!is_constant(e))
-            return false;
+    } else if (is_constant(p) && is_constant(e)) {
         levels p_ls = const_levels(p);
         levels e_ls = const_levels(p);
         while (!is_nil(p_ls)) {