Rebuild tactic state issue

[toontran]

Hello everyone,

I'm dabbling into the code and saw the following issue while looking at tactic_state.lean

Add the following example at the end of tactic_state.lean file.

example (α : Type) (a : nat): a=a := begin
induction a,
refresh_tactic_state,  -- check that tags are still there
end

Then after induction a tactic, the info view shows:

2 goals
case nat.zero
α: Type
⊢ 0 = 0
case nat.succ
α: Type
a_n: ℕ
a_ih: a_n = a_n
⊢ a_n.succ = a_n.succ

While after refresh_tactic_state, it shows:

2 goals
case nat.zero
α: Type
⊢ 0 = 0
case nat.succ
α: Type
a_n a_ih: 1
⊢ nat.succ a_n = nat.succ a_n

Notice type of a_n and a_ih doesn't show the appropriate ℕ and a_n = a_n anymore.

Thank you for checking!

[toontran]

I further inspected the list of declarations created, which shows that the type of the declarations seems to be off as well:

[build_context_aux] new_decl: {local_decl2 .
unique_name := 0._fresh.432.638,
pp_name := α,
expr_type := 1,
bi := default,
type := (some Type),
prev := none
},
frozen := ff,
ld := (some {local_decl .
      unique_name := 0._fresh.432.638,
      pp_name := α,
      type := Type,
      value := none,
      bi := default,
      idx := 0,
      })
[build_context_aux] New_decl: {mvar_decl .
unique_name := _mlocal._fresh.432.640,
pp_name := _mlocal._fresh.432.630,
expr_type := 2,
local_cxt := [α],
type := (some eq.{1} nat nat.zero nat.zero),
assignment := none,
}
[build_context_aux] new_decl: {local_decl2 .
unique_name := 0._fresh.432.642,
pp_name := a_n,
expr_type := 1,
bi := default,
type := (some 1),
prev := (some 0._fresh.432.638)
},
frozen := ff,
ld := (some {local_decl .
      unique_name := 0._fresh.432.642,
      pp_name := a_n,
      type := 1,
      value := none,
      bi := default,
      idx := 1,
      })
[build_context_aux] new_decl: {local_decl2 .
unique_name := 0._fresh.432.645,
pp_name := a_ih,
expr_type := 1,
bi := default,
type := (some 1),
prev := (some 0._fresh.432.642)
},
frozen := ff,
ld := (some {local_decl .
      unique_name := 0._fresh.432.645,
      pp_name := a_ih,
      type := 1,
      value := none,
      bi := default,
      idx := 1,
      })
[build_context_aux] New_decl: {mvar_decl .
unique_name := _mlocal._fresh.432.647,
pp_name := _mlocal._fresh.432.635,
expr_type := 2,
local_cxt := [α, a_n, a_ih],
type := (some eq.{1} nat (nat.succ a_n) (nat.succ a_n)),
assignment := none,
}