coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coq hangs on setoid_replace

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] coq hangs on setoid_replace
Date: Wed, 17 Dec 2014 16:45:29 -0800

I am trying to do seemingly straightforward rewriting using 'setoid_replace'
but this tactics call hangs indefinitely without giving any error messages.
Are there are any recommended ways to debug/fix this?

Using just 'replace' on the same terms works, but it using 'eq' instead of
the equality relation I need to use.

Sincerely,
Vadim Zaliva

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

[Coq-Club] coq hangs on setoid_replace, Vadim Zaliva, 12/18/2014
- Re: [Coq-Club] coq hangs on setoid_replace, John Wiegley, 12/18/2014
  - Re: [Coq-Club] coq hangs on setoid_replace, Vadim Zaliva, 12/18/2014