The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello

I'm planning some development with uses sets in various places and my
(preliminary) experience is that the Sets libraries that ship with Coq
are somewhat cumbersome to work with. 

Has anyone used this for some (larger) development? I'm not overly
worried about having to assume classical logic and various
extensionality axioms. I'm more interested in increased automation for
the set reasoning part.

The tactic "eauto with sets" only works in relatively few cases, even
after including Finete_sets_faacts which in turn exports almost about
the whole library on sets.

(Notation is also not an issue, this I have taken care of)

-- 
Regards
Christian Doczkal