fix(library/tactic/tactic_state): goal pp problem reported by Jared

src/library/tactic/tactic_state.cpp

@@ -131,12 +131,13 @@ format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) con
 }
 
 format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) const {
-    bool inst_mvars            = get_pp_instantiate_goal_mvars(get_options());
+    options opts               = get_options().update_if_undef(get_pp_purify_locals_name(), false);
+    bool inst_mvars            = get_pp_instantiate_goal_mvars(opts);
     metavar_decl decl          = *mctx().get_metavar_decl(g);
     local_context lctx         = decl.get_context();
     metavar_context mctx_tmp   = mctx();
     type_context ctx(env(), get_options(), mctx_tmp, lctx, transparency_mode::All);
-    formatter fmt              = fmtf(env(), get_options(), ctx);
+    formatter fmt              = fmtf(env(), opts, ctx);
     if (inst_mvars)
         lctx                   = lctx.instantiate_mvars(mctx_tmp);
     format r                   = lctx.pp(fmt);

tests/lean/pp_goal_issue.lean

@@ -0,0 +1,15 @@
+constant f : (nat → nat → Prop) → Prop
+
+example (h1 : false) : ∀ (a b c : nat), a = 0 → b = 0 → f (λ x y, a + x = b + c + y) :=
+begin
+  intros x x y h h, -- Force name clash
+  trace_state,
+  contradiction
+end
+
+example (h1 : false) : ∀ (a b c : nat), a = 0 → b = 0 → f (λ x y, a + x = b + c + y) :=
+begin
+  intros,
+  trace_state,
+  contradiction
+end

tests/lean/pp_goal_issue.lean.expected.out

@@ -0,0 +1,10 @@
+h1 : false,
+x x y : ℕ,
+h : x = 0,
+h : x = 0
+⊢ f (λ (x_1 y_1 : ℕ), x + x_1 = x + y + y_1)
+h1 : false,
+a b c : ℕ,
+a_1 : a = 0,
+a_2 : b = 0
+⊢ f (λ (x y : ℕ), a + x = b + c + y)