Regression in latest nightly

[david-christiansen]

The following code from a blog post isn't working in the latest nightly:

def search {α} (f : Nat → Option α) (start : Nat) (to : Nat) : Option α :=
  match f start with
  | .some x => .some x
  | .none =>
    if start < to then
      search f (start + 1) to
    else
      .none
termination_by to - start

theorem search_const_none {α} (start to : Nat) :
    search (α := α) (fun _ => .none) start to = .none := by
  unfold search
  split
  · exact search_const_none (start + 1) to
  · rfl
termination_by to - start

The highlighting code says that the recursive occurrence of search_const_none isn't present in the environment, and some printf-debugging shows that this is indeed the case when we use the environment saved in the context info in the info tree.