The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Sun, Aug 3, 2014 at 1:55 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

PS ... and if I write this:

Definition nonsense ( x : un ) := match x with y + 2 => 0 end .

I get this:

> Toplevel input, characters 20-83:
> Anomaly: Uncaught exception Not_found(_). Please report.

That is a bug which you should report on the bug tracker.  (If you don't have an account, I could report it for you, if you want.)