Adding phantom types to discriminate normalized goals, and adding a way to
observe non-normalized goals.
Using non-normalized goals in tactic interpretation.