extend these iterators to other collections - like hypotheses, evars, etc.

[jonleivent]

I like the interface to this tactic (although the "run" keyword doesn't do much) - would it be hard to extend this interface to iterate over other useful lists, such as the list of hypotheses in the current goal (in both forward and reverse order), and the list of evars?

I have my own Ltac library of iterators over hypotheses, and it has been very useful - but I would not mind at all if it was replaced by an extension of this plugin.

Perhaps using some symbols to fill in for the "pseudo" hint db name of the hypotheses and evars. One obvious one would be to use "?" as the name for the evars, so that:

foreach [ ? ] run f.

would invoke f once for each evar. Perhaps "*|-" would work as the name for hypotheses?

foreach [ *|- ] run f.

And of course a way to reverse the order - perhaps by putting the word "reverse" in somewhere.

Another collection that would be useful to iterate over: constructors of an inductive type. Maybe this syntax:

forach [ typename: ] run f.

Other collections: names in a module (so as to do a Search via Ltac), section vars, etc.

-- Jonathan

[gmalecha]

These all seem like very good ideas. Some of them I have a sense of how to implement. I'll see if I can look a bit more into this in the coming week.

Hint databases are probably actually the most complex because there are many things inside of a database, e.g. extern tactics.

[gmalecha]

I added the premises iterator (15ac7f5) and coded up some hooks to other iterators, but they are not implemented yet.

I also dropped the 'run'.