From fe66e2aa4a40d4a118a8ea930eaa599e65298421 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Dec 2015 09:04:11 -0800
Subject: [PATCH] fix(tests/lean): subtype notation is not in the top-level
 anymore

---
 tests/lean/630.lean         | 2 +-
 tests/lean/print_ax1.lean   | 1 +
 tests/lean/print_ax2.lean   | 2 +-
 tests/lean/print_ax3.lean   | 1 +
 tests/lean/run/sub_bug.lean | 2 +-
 tests/lean/subpp.lean       | 2 +-
 tests/lean/subst_bug.lean   | 2 +-
 7 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/tests/lean/630.lean b/tests/lean/630.lean
index 573e67d71..596d2c7c8 100644
--- a/tests/lean/630.lean
+++ b/tests/lean/630.lean
@@ -1,5 +1,5 @@
 import data.pnat
-open pnat
+open pnat subtype
 
 print pnat
 
diff --git a/tests/lean/print_ax1.lean b/tests/lean/print_ax1.lean
index 912e0dbde..ed0c9f99c 100644
--- a/tests/lean/print_ax1.lean
+++ b/tests/lean/print_ax1.lean
@@ -1 +1,2 @@
+open subtype
 print axioms
diff --git a/tests/lean/print_ax2.lean b/tests/lean/print_ax2.lean
index 912e0dbde..efdcf5db5 100644
--- a/tests/lean/print_ax2.lean
+++ b/tests/lean/print_ax2.lean
@@ -1 +1 @@
-print axioms
+open subtype print axioms
diff --git a/tests/lean/print_ax3.lean b/tests/lean/print_ax3.lean
index d2032e09d..753e702c7 100644
--- a/tests/lean/print_ax3.lean
+++ b/tests/lean/print_ax3.lean
@@ -1,3 +1,4 @@
+open subtype
 theorem foo1 : 0 = (0:num) :=
 rfl
 
diff --git a/tests/lean/run/sub_bug.lean b/tests/lean/run/sub_bug.lean
index ed552b2db..23187a6df 100644
--- a/tests/lean/run/sub_bug.lean
+++ b/tests/lean/run/sub_bug.lean
@@ -1,3 +1,3 @@
 import data.nat
-open nat
+open nat subtype
 check { x : nat | x > 0}
diff --git a/tests/lean/subpp.lean b/tests/lean/subpp.lean
index 01f46bd4b..c584ea780 100644
--- a/tests/lean/subpp.lean
+++ b/tests/lean/subpp.lean
@@ -1,4 +1,4 @@
 -- import data.subtype
-open nat
+open nat subtype
 
 check {x : nat| x > 0 }
diff --git a/tests/lean/subst_bug.lean b/tests/lean/subst_bug.lean
index f174f9d73..a086dd62a 100644
--- a/tests/lean/subst_bug.lean
+++ b/tests/lean/subst_bug.lean
@@ -1,4 +1,4 @@
-example (f : nat → nat) (a b : nat) : f a = a → f (f a) = a :=
+open subtype example (f : nat → nat) (a b : nat) : f a = a → f (f a) = a :=
 begin
   intro h₁,
   subst h₁ -- ERROR