coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 |
- [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
- RE: [Coq-Club] Removing type class instances, Soegtrop, Michael, 04/23/2018
- Re: [Coq-Club] Removing type class instances, Matthieu Sozeau, 04/23/2018
Archive powered by MHonArc 2.6.18.