coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Removing type class instances

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Removing type class instances
Date: Mon, 23 Apr 2018 15:30:16 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga01.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:upcvpxKChPhuKkSdGtmcpTZWNBhigK39O0sv0rFitYgeLv7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicZOTAk7GHZhM9+jKxZrxKguxNwzJXZb5uJOPZiZK7RYc8WSGhHU81MVyJBGIS8b44XAuYPIOhYqJfyp1QSrRukAgmsHPvjwSJPiH/3waI60/4uHh/C3AAuAtkDt3HUrNTpO6cSS++60q3IwS/Yb/NRxzj955TIcgomofGURr9wcMzRyVUxGAPBlFmftYvlPzaM2+kLrmOV4e1gVee1hG4mrQF8ujmvxsEwiobXgoIZ0E3L+jt/zY0oJtO4UFZ2bcOgHZdOrS2XN4t7TtkiTm12oio3yb4LtYamcCULxpkr3RDSZvKdf4SW7B/uUPydLSp7iX57YL6zmhe//Ey6xuHiVsS530xGojRfntXRt30A2Bre4dWdRPRn5EeuwzOP2hjT6u5aJUA0krLWK5suwrEqipYfrF7PHi7wmEXqkqCWcl8o9fSv6+Tiernmp5mcOJFoigzmL6gjntKzDf44PwUORWSW+fqw2Kfg8ED6WLlKi+c5kqjdsJDUP8Qboau5DhdQ0oYi9xm/Dy2p38ocnXUdN1JFfwyIj4f1O1HUJ/D4Feyyg1WqkDd32f/GOqftDYnKLnjGiLvhZ6py61ZAyAovytBS/45bCrYYIP7qRkDxsMHYAQQiPgyvw+fnDc192ZkEVWKOBK+ZKqLSvkWS6uIhOenfLLMS7Xz2LOFg7Przh1c4n0UcdO+nx9FfPHu/B7FtJ1iTSXvqmNYIV2kQ6FkQVuvv3Re5VjNce2y1R+Z0wzAwCIurCc2LEoWsi7yI0SP9BZpbaXxcDUikEHH0eoHCUPAJPnHBavR9myAJAODyA7Qq0guj4VejmuhXa9HM8yhdjqrNkd185undjxY3rGUmDsKB3mXLRGZxzDpRG20GmZtnqEk48W+tlLBiiqUBR91V+/5NFAw9MMyElrEoO5XJQgvEO+yxZhOmT9GhWG5jS904m4ZIYkBhFtHkhRfGjXKn

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