The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I get "Anomaly: File "toplevel/himsg.ml", line 699, characters 2-8: Assertion failed.

Please report." on [reflexivity] and [apply eq_refl], but [exact eq_refl] and [refine eq_refl] both work fine.  This is in Coq 8.4.  I don't currently have the time to make a small working example, but does anyone have any idea what might be going on here?

Thanks,

Jason