The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> On 07/02/2017 19:02, Ralf Jung wrote:
>> I was told once that just doing "Set ...." would set options in a way
>> that they would apply through one, but *not* two levels of "Import" (and
>> an arbitrary number of "Export"), but that doesn't actually seem to be
>> the case.
> 
> Being the one who told you that, I feel guilty. Still, this seems like a
> bug to me, and I was pretty sure that this was the expected behaviour.
> I'll have a look when I have spare time.

Great, thanks.
No reason to feel guilty though, Coq is a nasty beast, seems like it can
even confuse its developers. ;)

> In the meanwhile, ****PLEASE DO NOT USE LOAD****. Pardon the
> capitalizing, but that's important matter here. This command is a rather
> horrendous hack that SHOULD NOT appear in proper development files. It
> is borderline to use it in interactive proofs, and it should not be used
> anywhere else. I even think it is more or less bound to be removed at a
> future stage.

Horrendous hacks seem to be what we use frequently. ;)
It seems though then as if we don't really have any option right now for
setting options just inside a library.  Probably we will end up not
doing anything then, just sticking with what we got -- and continue to
try and remember to set "Default Proof Using" in every single file.

Kind regards,
Ralf