Ssreflect Users Discussion List

[Jason Gross <>]

I have run into a number of cases where ssreflect's rewrite will loop forever (or at least for a number of minutes), while Coq's rewrite (accessed by doing [Ltac coq_rewrite H := rewrite H.] before I've imported ssr) will succeed instantly.  I'll set my scripts on generating a minimal example, but I was wondering if anyone else has encountered this problem, and if anyone could enlighten me as to why this might be happening, or at least to the differences between Coq's rewrite and ssr's rewrite.

Thanks,

Jason