On Mon, 12 Sep 2011 08:20:44 +0200, Hendrik Tews <[email protected]>
wrote:
> Tom Prince <[email protected]> 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
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
