coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e AT x80.org (Emilio Jesús Gallego Arias)
- To: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Typeclass confusions
- Date: Sat, 24 Jun 2017 17:42:58 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-a.ensmp.fr
- Ironport-phdr: 9a23:t8YCnxXUoPY4ZKtpK3MXu/OBXBbV8LGtZVwlr6E/grcLSJyIuqrYYx2Gt8tkgFKBZ4jH8fUM07OQ6PG/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdwIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2ycZYBD+0PPehWrYbzpFUBohSiCgS3GOPj1iVFimPq0aAg0eksFxzN0gw6H9IJtXTZtMv6ObwdUO220KXE1zLDb+lZ2Tzg7ITGfRUhofCIXbJxdsra1E0hGB3ejk2KsozuIjKb2f4Js2if8eVgWuWvgHM7pgFrozig3NwshozPi4kIyV7E7T10zJsxKNC3UkJ3f8OoHZRKuy2HN4Z7QdkuT3xmtSs50rELup+2cDILxZkl3RLSb+aLf5WV7h/jUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtFsjZKnsDQtnAQzxzc8M6HRuJn/kemwzmP0gHT6udLIUwtj6XXMYAuwrgrlpoWqUTPBCH2mF/ugK+XcEUr5PSo5vz6brjiqZKQLZF4hhzxP6g0h8CyAec1PhITU2WV+umwzLjj8lf4QLVOgP02iK7ZsJXCKMsFvaO4DAxY3po55xa4FTem38wUnWMbI1JdZBKHk4/pNknSL/D/FPezmkijkDN2x//dJbDhGZXMLn3bkLj7Z7p96khcyBAyzd9F/Z5UBKsBc7rPXRrevdHEBxlxHA2wyev9FJ0p2YoTRWuJRKCYNKnfq0Og6+Q0Zu2dY4lTtiyreNY/4Pu7gFcpyQdberOmlds6bXG8H/MuAUiC82Gkrd4FFWoFuUIXVu3jkxzRAnZoe3+uUvdktXkAA4W8ANKGH9j1jQ==
- Organization: X80 Heavy Industries
Gaetan Gilbert
<gaetan.gilbert AT ens-lyon.fr>
writes:
> You mean the error gotten by reverting
> a7ea32fbf3829d1ce39ce9cc24b71791727090c5 is in this case better?
Well, certainly I can't make sense of what that commit means.
Looking at the changes and commit message, it looks like the commit was
unfinished, maybe it slipped-in accidentally?
In fact it was coming from a 8.5 merge it seems, so that could explain
it.
E.
- [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Abhishek Anand, 06/24/2017
Archive powered by MHonArc 2.6.18.