On Mon, 12 Sep 2011 08:20:44 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de> 
wrote:
> 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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to