There is too much shadowing of standard modules about coq-ext-lib HOT 4 CLOSED

This is supposed to be fixed in 8.5 when libraries will not be included with -R (which itself is horribly broken). Until that fix is in I have been requiring ExtLib locally for projects using _CoqProject or .dir-locals.el and requiring it with -I, e.g. -I <path-to-ext-lib-theories> -as ExtLib. This makes it so that you can Require Import Bool and get Coq's Bool and you can Require Import ExtLib.Data.Bool to get ExtLib's definitions surrounding bool.

The only solution that seems to work in 8.4 would be to prefix every file with something, e.g. Bool -> ELBool or something like that which just seems very ugly to me. That is the purpose of namespacing modules.

Alternatively, you can tweak the Software foundations using some scripts to make them require full Coq paths, e.g. convert Require Import Bool to Require Import Coq.Bool.Bool.

What do you think is the best solution?

from coq-ext-lib.

If 8.5 is going to resolve this question, then I think just waiting for 8.5 is the best solution. :)

from coq-ext-lib.

From what I've heard it will not include user-contrib using -R which will solve the problem.

from coq-ext-lib.

This is solved in 8.5

from coq-ext-lib.