coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Removing type class instances
Date: Mon, 23 Apr 2018 08:16:47 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.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:PiKNsxf40quUv63YvD3kTz44lGMj4u6mDksu8pMizoh2WeGdxcS5bB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhpgBwzIHPbY6PKPZzernQcc8GSWZfWMtaSixPApm7b4sKF+cNM/tWr47jqFsBsRu+Hw6sBPv3xjRVgXH23LE10+Q7Hg7Y2AwsEc8FvXPRrNX0KKgSUfq6w7fMzTnZdPNW3iny6IfUchA7pvGMRal9ccvXyUkzCQzFik+cppDiPzOQz+kAtXWQ4eRnVeKqkWEnqgdxryCuxscqlonGmIYVxkrZ+ipnxos+ON62SFZjbNK5FJZcqTuWOot2T884Q2xkpjw2x74FtJKjYSQHyZoqywTRZvGJaYSE/BzuWeKLLTtlh39pZaqziwuz/EWk0OHwSMm53VlQoiZbiNXAq3EA2hPV58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJp4kzb4/jIYfvVnZEi/3nkX2kLGZdkE+9ue07OTnZ63qpp6aN4BqlgHzKrkil8ihDegiMgUDX3KX9OSi2LH5/kD0Q61GjvgsnanYtJDaK94bpqm8AwJN14Yj6gqwDze839sGmXkLNklFeBWZgIjmJ1HOOvf4De+kjlStljdr2+7JPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2O3IP88ovXqkHURmFkHfKDv04FdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQjIajleaGqoWLp4rhQ6A4KvAIOJDtSogbeB1Sq/WIZRa29aEFeUOXbua4iAHfwLbXTBcYdajjUYWO35GMca3ha0uVqikus1Hq/v4iQd8Knb+p1w7uzXmws18GUtXcWbz2yJCWpzmzFRHmNk7OVEuUV4j2y7/+1gmfUBTI5S4e9EVkExMpuOl7UnWeC3YRrIe5KycHjjQtiiBmhuHNc+yodXJUd7B9imyBvE2njyDg==

Dear Coq Users,

I thought that type class instances can be removed with Remove Hints (although it isn’t documented this seems to be the obvious way). But it doesn’t seem to work (8.7.2):

Require Import Morphisms.

Require Import Classes.Morphisms_Prop.

Remove Hints all_iff_morphism : typeclass_instances.

Print Instances Proper.

The Print output still contains “all_iff_morphism” and it still seems to be used.

What is the proper way to remove type class instances?

Best regards,

Michael

P.S.: I want to do this primarily for demonstration purposes.

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