Typos in comment.
In Ltac's exact tactic: avoid checking the type of the term twice.

Following a remark by Jason Gross and Daniel Grayson.