The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

Specialized tactics should be able to make working with finite sets
much, much easier.  In particular, there should be a certain class of
goals that could be immediately solved by a specialized tactic if
their truth is justified by your hypotheses (or, to be more precise,
the subset of your hypotheses not involving first-order quantifiers).

I am tempted to write my own such tactic for the FSets library, but in
order to avoid duplicating effort, I should first ask:  Has anyone
else already done this?  Which tactics defined in FSets.OrderedType
and the other FSet libraries are intended for use by clients of the
library?  Do they have any documentation or specification other than
the text of the "Ltac" defintion?  (Deducing the intended behavior and
scope of a tactic from the code of its definition is not an easy
task.)

-Aaron