From 3f9549485fd0734c7fa3c0a2c99ba3e204a0e88d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Dec 2015 11:24:37 -0800
Subject: [PATCH] feat(frontends/lean/parser): restore config options in the
 end of sections/namespaces

---
 src/frontends/lean/parser.h                | 2 +-
 tests/lean/634d.lean.expected.out          | 2 +-
 tests/lean/ctxopt.lean.expected.out        | 2 +-
 tests/lean/ftree.lean                      | 2 +-
 tests/lean/run/blast_grind1.lean           | 1 +
 tests/lean/sec_param_pp2.lean.expected.out | 4 ++--
 6 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index a4949e029..844596df6 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -231,7 +231,7 @@ class parser {
     friend environment namespace_cmd(parser & p);
     friend environment end_scoped_cmd(parser & p);
 
-    void push_local_scope(bool save_options = false);
+    void push_local_scope(bool save_options = true);
     void pop_local_scope();
 
     void save_snapshot();
diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out
index d18dece02..a942294a2 100644
--- a/tests/lean/634d.lean.expected.out
+++ b/tests/lean/634d.lean.expected.out
@@ -3,7 +3,7 @@ _root_.A : Type₁ → Type₁
 A : Type.{l} → Type.{l}
 _root_.A.{1} : Type₁ → Type₁
 P : B → B
-_root_.P.{1} : Π {n : ℕ}, ℕ → ℕ
+_root_.P : Π {n : ℕ}, ℕ → ℕ
 P : B → B
 _root_.P.{1} : ?B → ?B
 @P 2 : B → B
diff --git a/tests/lean/ctxopt.lean.expected.out b/tests/lean/ctxopt.lean.expected.out
index 2e5262270..d75e4dd64 100644
--- a/tests/lean/ctxopt.lean.expected.out
+++ b/tests/lean/ctxopt.lean.expected.out
@@ -1,2 +1,2 @@
 @id Prop true : Prop
-@id Prop true : Prop
+id true : Prop
diff --git a/tests/lean/ftree.lean b/tests/lean/ftree.lean
index 2ec6f1b72..6f9e887dd 100644
--- a/tests/lean/ftree.lean
+++ b/tests/lean/ftree.lean
@@ -26,6 +26,6 @@ inductive ftree (A : Type) (B : Type) : Type :=
 leafa : A → ftree A B |
 leafb : B → ftree A B |
 node  : (list A → ftree A B) → (B → ftree A B) → ftree A B
-
+set_option pp.universes true
 check ftree
 end implicit2
diff --git a/tests/lean/run/blast_grind1.lean b/tests/lean/run/blast_grind1.lean
index cce566bb6..08c382c10 100644
--- a/tests/lean/run/blast_grind1.lean
+++ b/tests/lean/run/blast_grind1.lean
@@ -27,5 +27,6 @@ by blast
 example (a : nat) : a = 0 → (λ x, x + a) = (λ x, x + 0) :=
 by blast
 
+set_option trace.blast true
 example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
 by blast
diff --git a/tests/lean/sec_param_pp2.lean.expected.out b/tests/lean/sec_param_pp2.lean.expected.out
index 2c7b0bdac..3d6831912 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.{l_2} : ?B a → (A → ?B a → A) → A
-id2.{l_1 l_2} : ?A → (Π {B : Type.{l_2}}, B → (?A → B → ?A) → ?A)
+id2 : ?B a → (A → ?B a → A) → A
+id2 : ?A → (Π {B : Type}, B → (?A → B → ?A) → ?A)