The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Michael,

  Remove Hints effectively removes the instance from the hint database but not the other database of instances

used by Print Instances (use Print HintDb typeclass_instances to check), i.e. they are now out of sync. There should

rather be a Remove Instance command that properly removes the instance also from that database (which, AFAIR,

is only used for Print Instances actually), maybe you can submit a Coq issue about this?

Best,

-- Matthieu

On Mon, Apr 23, 2018 at 10:17 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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