coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Removing type class instances

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Removing type class instances
Date: Mon, 23 Apr 2018 15:49:25 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f176.google.com
Ironport-phdr: 9a23:R3krcx2DAsS37kI7smDT+DRfVm0co7zxezQtwd8Zse0QL/ad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6yaJEAD/YdPeZYronyuUYOpgajCwmrBeLg1CVHhmLr1qA91uQuCx3G3BA6ENILq3nUqc/6NLsOUe+vyanE1zLDb+lZ2Trk7oXDbx4vofaJXb1qcMrRz1EiFwzCjlWXpozlOy2a2v4RvGic6upsTeOvi2g7qw5vpjij3NojhZfPi4kIyV7E7T10zJgpKdC8UkJ2Yt6pHIFNuy2ENIZ6WN4uTmNptSs817YIo4S0fDIQx5Qi3xPfa+KIc4yP4h/7UeaeOzZ4hHZ8dLOxnRa+7VGsyuPhWsS20VtGtCVFkt7LtnAC0xzc9NKLRed6/kekwTqP1gbT5f9YIU0si6bXN5oszqQzm5cTq0jPAzH6lUbsgKOLdEgp+/Ck6+H9bbXnop+cOZV0igb7Mqk2n8ywG/g4MhQOX2ia5+u8yafv/Vb+QLRLkPI5iLTZvYvVJcQevKG5AgtV3pw/5Ba4CjeqyM4YkmUfLFJZZBKHiJDkNE3JIPDhFPuwn1CskCpwyP3dJb3gApDNLmDZn7v7fLZ97VRcyAspwtxF6ZJUEOJJHPWmUUjo8dfcExURMgquwu+hBs8u+JkZXDeqC7OFMKLfrBez4fAiKvTEMIocpCr0LtAg7uLyhHp/nkUSK/r6laALYWy1S6w1a36SZmDh149YQDU6+zEmRemvs2WsFDtaZnK8RaU5v2hpB4evDIOFTYeo0uXYgHWLW6ZOb2UDMWiiVG/yftzeCfIFdD6bJ4lmiDNWDeH8Gb9k7gmnsUrB85QiLufQ/XdG55fq1dww+PeL0B9rqmIyAMOa3GWACWpzmzFQSg==

Dear Michael,

The database used by typeclass resolution is the hint database, so Remove Hint works already, the other one is used solely for Print Instances.

Best,

-- Matthieu

On Mon, Apr 23, 2018 at 5:31 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Matthieu,

just to make sure I understood it: is it so that there are two databases, a hint database called “typeclass_instances” with the sole purpose of make the type class instances accessible to eauto and another database which is used by automatic type class resolution?

I will create an issue for this.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Removing type class instances, Soegtrop, Michael, 04/23/2018
- Re: [Coq-Club] Removing type class instances, Matthieu Sozeau, 04/23/2018
  - RE: [Coq-Club] Removing type class instances, Soegtrop, Michael, 04/23/2018
    - Re: [Coq-Club] Removing type class instances, Matthieu Sozeau, 04/23/2018