alias ignores noncomputable section

[YaelDillies]

alias correctly handles noncomputable on a def, but not noncomputable on a section:

import Batteries.Tactic.Alias

noncomputable def foo : Nat := Classical.choice sorry

alias bar := foo -- works fine

noncomputable section

def baz : Nat := Classical.choice sorry

alias quux := baz
-- failed to compile definition, consider marking it as 'noncomputable' because it depends on 'baz',
-- and it does not have executable code