fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning.

Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
2014-09-26 09:42:31 -07:00 · 2014-09-26 09:42:31 -07:00 · 631ebc6c4b
commit 631ebc6c4b
parent 6bf905aea8
2 changed files with 1 additions and 2 deletions
--- a/tests/lean/uni_bug1.lean
+++ b/tests/lean/uni_bug1.lean
@ -1,4 +1,4 @@
-import data.nat data.prod
+import data.nat.basic data.prod
 open nat prod

 variable R : nat → nat → Prop
--- a/tests/lean/uni_bug1.lean.expected.out
+++ b/tests/lean/uni_bug1.lean.expected.out
@ -1,2 +1 @@
-uni_bug1.lean:2:0: warning: imported file uses 'sorry'
 f 1 0 (Rtrue (pr1 (pair 1 0)) 0) : nat