On Mon, 12 Sep 2011 08:20:44 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de> 
> Tom Prince <tom.pri...@ualberta.net> writes:
>    Some developments don't fully qualify their imports, and so coqdep gives
>    warning about ambiguous imports. Allow these developments to use
>    auto-compilation mode anyway.
> Could you describe an example? What is coqdep printing in these
> cases?

*** Warning: in file categories/orders.v, 
    required library setoids matches several files in path
    (found setoids.v in varieties, theory and categories; used the latter)
ProofGeneral-devel mailing list

Reply via email to