The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

I think currently there is no better way than manual "with mybase".

Maybe we could add an option "Set Default HintBase mybase", then you 
could use regular option scoping.

ie either put "Set" at the top of every file or module you want it in, 
or "Export Set" in FooOptions.v (where Foo is your project) and import 
that everywhere you want it in.


Gaëtan Gilbert

On 14/11/2018 20:27, Armaël Guéneau wrote:
> 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