The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Dear coq-club,

I just finished a Coq development, which I now want to publish, and I'm
facing the following issue:

While doing my development, I added a good number of hints (mainly Hint
Resolve and Hint Constructor) to the default database (ie "core" if I'm
not mistaking).
This was because it's much more convenient to write "eauto" everywhere
than "eauto with mybase" which is a lot more annoying to type(!).

But now, anyone loading my development will get its core database
polluted with my hints, which is very bad.

How can I refactor my project to avoid this?

My project spans across several files, and I'd like to share the hints
across the files, so delimiting them within a Section doesn't quite work
I think.
I could do "Tactic Notation go := eauto with mybase" but that doesn't
scale to [eauto using ... with ...].
Using "eauto with mybase" manually is annoying because I use the tactic
in a lot of places.

Even if it doesn't exist currently, I wonder what would be a nice
solution to this problem. Having a way of defining variants of (e)auto
that use different hint bases (while supporting all the [using ..],
[with ..] variants) sounds useful, I think?

— Armaël