Skip to Content.
Sympa Menu

coq-club - [Coq-Club] setoid rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] setoid rewriting


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page