The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Is the following a bug?  It certainly appears to be a different behavior than the Reference Manual suggests:

Goal forall (n : nat), n = S n -> False.
  intros n H.
  simplify_eq H.

Instead of behaving like discriminate or injection (both of which fail on H), the above simplify_eq H just copies H into the consequent. 

-- Jonathan