The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I just debugged an infinite loop in typeclass eauto that was apparently 
due to Existing Class causing instances created afterwards to become 
Existing Instances, even if not explicitly declared as such.  I had 
declared "Existing Class eq", and really only wanted a very few cases of 
eq to be considered instances, but some later equalities automagically 
became instances (I can see them via Print Hints in the 
typeclass_instances db).

First of all - is this a feature or a bug?  Secondly, if a feature, is 
there a way to turn it off, at least for particular Classes?

-- Jonathan