coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with constructive rewriting

From: "John Wiegley" <johnw AT newartisans.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Problem with constructive rewriting
Date: Fri, 12 May 2017 17:11:48 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f174.google.com
Ironport-phdr: 9a23:EAOGSxUU8Sz6GrPbsQQ/C3gXYzPV8LGtZVwlr6E/grcLSJyIuqrYbBCEt8tkgFKBZ4jH8fUM07OQ6PG8HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLd9IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2ycZYBAOgPM+ZfrIf9qVUBohSiCgS3GOPj1iVFimPq0aAgz+gsFxzN0gw6H9IJtXTZtNv5OqMVUeC1yqnD0DXMb/JI1jfy7IjHbBAgrf+RVr93c8rRzkkvFwXLj1iLr4zqIT2U2f4Xs2iH7upgTvigi2g8qw1rvjevwcIsh5DPi4kIxF7E8iB5z5w0Jd2+UEN7Z8CrEZVKuCGAK4t2Q9giTHtuuCYh0LEJpZm7fC0MxZ86xBDfc+SKf5aU7h/nTuqcIjd1iGh4dL+7mRq+61Wsx+/zW8Ws0ltHrzBJnsfCu30CzRDe68yKRuFg8kqu3TuC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBir2l1/3jK+Sb0kk4uao5/j+brXou5ORNYB5hhvxMqQpncy/DuA4PRYUU2eH/uS80aXv/Uz/QLpUkv07irfVvIzeKMgBpaO0AxVZ3psn5hqhFTuqzdYVkHYfIFJAYh2HjozpO1/UIPD/CPeym1askTlqx//YMb3hBovCL3jYnbfueLZy8U9cyA4pwd9D4JJUD6kNIOjvVU/pqNzYEhg5PhSozObgEdVxz58RWWaSAqCCK67Sql+J5uc3I+aWfoMVuTD9K+Ik5/H0l3M5l0UdLuGV2s41YWu/GLxJOUKCejK4gN4aFmEFpA0lV73Ch1iLUDoVbHG3CfES/DY+XciECofFDr+sjbOF0TbxVslUYWBAFXiKHGjhbZmFQP4Kc2SZJco3wW9MbqSoV4J0jULmjwT90bcya7OMoiA=
Organization: New Artisans LLC

>>>>> "JG" == Jason Gross
>>>>> <jasongross9 AT gmail.com>
>>>>> writes:

JG> Can you make a small example and report it on the bug tracker? It seems
JG> like something in setoid_rewrite might be dropping universes or something,
JG> since there's no explicit "universe inconsistency" message.

Thanks, I've logged it as issue #5521 with a reduced case. Interestingly
enough, if I remove two fields from the Isomorphism type class, it works, but
not with them present (and they are needed).

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
- <Possible follow-up(s)>
- [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
  - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
    - Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
      - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
        
        Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/13/2017