The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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.

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.

Thanks for your attention,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature