The Coq mailing list

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

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