Difference between coq options -Q and -R about unimath HOT 1 CLOSED

Great! I will implement it.

On Sun, Sep 27, 2015 at 2:15 PM, Benedikt Ahrens [email protected]
wrote:

from what I understand, -Q only adds one directory to the search path
under the given name, whereas -R adds the directory and all its
subdirectories.

Maybe it would be safer to use -Q ?
As a consequence, Imports would always need to use the fully qualified
name UniMath.Package.file, but we are doing this anyway.

This would allow having files of the same name in different packages
without the risk of confounding them.

—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_159&d=AwMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=5IX9gfQRu4q7FsNB3nX_PUscXrDe5bUInUF-B2dHPVw&s=sL50Dya3c_MzyxB8Q6nihqjaUYoYVVfn5AM98droM0c&e=
.

from unimath.