From 6762f8ea9a7107e68a16e923fe077efba2a19635 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Jan 2020 13:49:42 -0800
Subject: [PATCH] test: old frontend exports at new frontend

We can now "see" exports made in the old frontend in the new one.

cc @dselsam @kha
---
 tests/lean/run/newfrontend1.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 09b56820d5..e279471fe7 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -27,9 +27,11 @@ set_option pp.all true
 
 #check foo 1
 
-#check foo 3 (c := Bool.false)
+#check foo 3 (c := false)
 
 def Nat.boo (a : Nat) :=
 succ a -- succ here is resolved as `Nat.succ`.
 
 #check Nat.boo
+
+#check true