Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Difference between [setoid_rewrite at 1] and [setoid_rewrite]?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Difference between [setoid_rewrite at 1] and [setoid_rewrite]?


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Difference between [setoid_rewrite at 1] and [setoid_rewrite]?
  • Date: Mon, 10 Mar 2014 04:34:38 -0400

Hi,
Can someone explain to me the difference between [setoid_rewrite ... at 1] and [setoid_rewrite ...]?  In particular, why might the first succeed when the second fails?  (This seems to me to be a bug, so I reported it, with a test case, at https://coq.inria.fr/bugs/show_bug.cgi?id=3253.)

Thanks,
Jason



Archive powered by MHonArc 2.6.18.

Top of Page