coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] setoid rewriting
Date: Mon, 1 Aug 2016 13:16:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f52.google.com
Ironport-phdr: 9a23:/OMqZBSIxPe2EZEoJjKQAYv9JNpsv+yvbD5Q0YIujvd0So/mwa64ZhON2/xhgRfzUJnB7Loc0qyN4vimBjFLuM3e+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0pMCYOl4XzBOGIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs0UVXmQT2ihBBwnb5VmuQIX4tirkv8J23TTcMMHrG+NnEQ++5rtmHUe7wBwMMCQ0pTna

Could anybody please explain to me why the following works:

repeat setoid_rewrite Foo at 1.

while this one does not (takes forever):

setoid_rewrite Foo.

I am using 8.5pl2.

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] setoid rewriting, Vadim Zaliva, 08/01/2016
- Re: [Coq-Club] setoid rewriting, Matthieu Sozeau, 08/07/2016
  - [Coq-Club] setoid rewriting, Pierre Courtieu, 08/07/2016
    - Re: [Coq-Club] setoid rewriting, Vadim Zaliva, 08/08/2016
      - Re: [Coq-Club] setoid rewriting, Matthieu Sozeau, 08/09/2016