The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

It's great that this is being looked into.

I would like to see recursive loads as an option, but only within each 
individual project.

> Require Import Bool.

This should always load Bool from the Coq standard library.

> which previously referred to Coq.Bool.Bool will now refer to this 
> ExtLib.Data.Bool. This is obviously a bad thing (since the user doesn't see 
> it, spooky action at a distance).

I would prefer to write Require Import ExtLib.Bool, rather than Require 
Import ExtLib.Data.Bool here. This could potentially differ from package to 
package if need be.

> I am wondering what the Coq community thinks about this issue. I can think 
> of two solutions/work-arounds:
> 1) Should it become best-practice to include files by their absolute names? 
> If so, should we special-case the standard library in some way so it does 
> not require absolute names?

It should at least be best-practice to never release a contribution that is 
not guarded by a namespace somehow.

> 2) Should Coq file resolution be changed to not be recursive by default?

I do prefer the recursive load as long as everything is not just dumped into 
the main namespace.

Cheers, and thanks to both Thomas and Gregory for looking into this.

/Jesper