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
- Re: [Coq-Club] setoid rewriting, Vadim Zaliva, 08/08/2016
- [Coq-Club] setoid rewriting, Pierre Courtieu, 08/07/2016
- Re: [Coq-Club] setoid rewriting, Matthieu Sozeau, 08/07/2016
Archive powered by MHonArc 2.6.18.