The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Ralf,

FWIW, `Load options.` would work for this minimalistic example.
I'm not so sure if it's useful in your setting.

-Anton

> On 3 Feb 2017, at 14:51, Ralf Jung 
> <jung AT mpi-sws.org>
>  wrote:
> 
> Hi all,
> 
> there are some Coq options ("Set ...") that we want to set in a
> particular way for all files in our library, but do not want to force on
> our users.  For example
> 
>  Set Default Proof Using "Type".
> 
> Right now, we have that line at the top of every file, but that clearly
> doesn't scale.
> 
> We got the advice to instead create a file, e.g. "options.v", put the
> settings in there, and import that file everywhere.  However, that does
> not seem to work, as the following testcase shows:
> 
> $ cat options.v
> Set Implicit Arguments.
> $ cat test.v
> Require Import options.
> (* Set Implicit Arguments. *)
> Definition id (A : Type) (a : A) := a.
> 
> Even though the option is set in "options.v", it is not in effect in
> "test.v".  I can of course change options.v to use "Global Set", but
> then the option will leak to everything that even imports test.v, i.e.,
> to every user of our library -- which we specifically tried to avoid.
> Using "Require Import" or "Require" in test.v also does not seem to make
> any difference.
> 
> Is there any way in Coq to set options in every file of a library
> *without* imposing these options on the user, and without repeating the
> option in every single file?
> 
> Kind regards,
> Ralf