The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I wanted to manually perform a "discriminate", and I did something
like :

Lemma Z : true = false → False.
refine (λ H, match H with eq_refl => True end).
Defined.

I am pretty sure it used not to work (I am on a 8.4 trunk version) on
8.3. So I was very surprised to see it working, and I feared a bug.

Print Z.

Hopefully returns something that I recognize to be correct. So now
pattern matching on Coq seems more clever than in 8.3. So I was
wondering from when such an improvement occured and if there was some
other nice improvement in the same spirit (I did not find it in the
Changelog…).