The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I am using 8.4pl6 and get into the situation where using ’setoid_rewrite’ or 
’setoid_replace’ tactics 
just hangs up there and does not terminate. Any advice on how this problem 
could be debugged?
Can I enable some trace to see what it is doing? I tried to extract a small 
example demonstrating
the problem but failed as my proofs depend on a couple of 3rd party libraries.

A related question: I wan to try this under Coq 8.5. Somebody posted once a 
link to web page
which shows status of some automated build check showing what libraries are 
compatible with
different coq versions. I could not find it. In particular I need both 
“CoLoR” and “math-classes”
to be able to try my proof under 8.5.


Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva