From e4071639f11d25e3c86dfdfaeb90e4baac85fa20 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 6 Jun 2016 12:55:12 -0400
Subject: [PATCH] fix(builtin_cmds): metavar_args should be false by default

---
 src/frontends/lean/builtin_cmds.cpp         | 2 +-
 tests/lean/check.lean                       | 2 +-
 tests/lean/check2.lean                      | 2 +-
 tests/lean/ppbug.lean                       | 1 +
 tests/lean/protected_test.lean              | 1 +
 tests/lean/protected_test.lean.expected.out | 6 +++---
 tests/lean/sec_param_pp2.lean.expected.out  | 2 +-
 7 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 2d67b2e98..224592fb6 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -118,7 +118,7 @@ environment check_cmd(parser & p) {
     auto tc = mk_type_checker(p.env());
     expr type = tc->check(e, ls).first;
     options opts          = p.ios().get_options();
-    opts                  = opts.update_if_undef(get_pp_metavar_args_name(), true);
+    opts                  = opts.update_if_undef(get_pp_metavar_args_name(), false);
     io_state new_ios(p.ios(), opts);
     auto out              = regular(p.env(), new_ios, tc->get_type_context());
     formatter fmt         = out.get_formatter();
diff --git a/tests/lean/check.lean b/tests/lean/check.lean
index 3a4e6f7c9..451c69de5 100644
--- a/tests/lean/check.lean
+++ b/tests/lean/check.lean
@@ -1,5 +1,5 @@
 import logic
-
+set_option pp.metavar_args true
 check and.intro
 check or.elim
 check eq
diff --git a/tests/lean/check2.lean b/tests/lean/check2.lean
index 210449e6e..eba96a0b4 100644
--- a/tests/lean/check2.lean
+++ b/tests/lean/check2.lean
@@ -1,3 +1,3 @@
 import logic
-
+set_option pp.metavar_args true
 check eq.rec_on
diff --git a/tests/lean/ppbug.lean b/tests/lean/ppbug.lean
index 0c95330f2..1d3cabb76 100644
--- a/tests/lean/ppbug.lean
+++ b/tests/lean/ppbug.lean
@@ -1 +1,2 @@
+set_option pp.metavar_args true
 check char.rec_on
diff --git a/tests/lean/protected_test.lean b/tests/lean/protected_test.lean
index 20f8757de..e3f46d456 100644
--- a/tests/lean/protected_test.lean
+++ b/tests/lean/protected_test.lean
@@ -1,3 +1,4 @@
+set_option pp.metavar_args true
 namespace nat
   check induction_on      -- ERROR
   check rec_on            -- ERROR
diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out
index 68342737a..dab5743a6 100644
--- a/tests/lean/protected_test.lean.expected.out
+++ b/tests/lean/protected_test.lean.expected.out
@@ -1,7 +1,7 @@
-protected_test.lean:2:8: error: unknown identifier 'induction_on'
-protected_test.lean:3:8: error: unknown identifier 'rec_on'
+protected_test.lean:3:8: error: unknown identifier 'induction_on'
+protected_test.lean:4:8: error: unknown identifier 'rec_on'
 nat.induction_on : ∀ n, ?C 0 → (∀ a, ?C a → ?C (succ a)) → ?C n
 le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
 le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
-protected_test.lean:8:10: error: unknown identifier 'rec_on'
+protected_test.lean:9:10: error: unknown identifier 'rec_on'
 le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1
diff --git a/tests/lean/sec_param_pp2.lean.expected.out b/tests/lean/sec_param_pp2.lean.expected.out
index 8c61bab16..9bf20db19 100644
--- a/tests/lean/sec_param_pp2.lean.expected.out
+++ b/tests/lean/sec_param_pp2.lean.expected.out
@@ -1,4 +1,4 @@
 id2 : (A → B → A) → A
 id2 : (A → B → A) → A
-id2 : ?B a → (A → ?B a → A) → A
+id2 : ?B → (A → ?B → A) → A
 id2 : ?A → (Π {B}, B → (?A → B → ?A) → ?A)