The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

So, I installed CoRN into ~/.local/share/coq/CoRN (the same thing would
happen when installing into ($COQLIB/user-contrib/CoRN), and then the coq
build failed, because it was picking up files there, (and failing due to
version mismatch). This is because CoRN contains model/Zmod/ZGcd.v and
Coq.Numbers.Integer.Abstract.{ZLcm,ZProperties} include an unqualifed ZGcd.

Clearly something should be done. But perhaps two things.
1) Coq shouldn't be looking there when compiling itself.
2) Module names should perhaps be looked for in the current hierarchy first.
   Otherwise, not fully qualified names can be accidently overriden by
   random other files in the search path (belonging to other packages).
   math-classes has, for example, misc/util.v so if it is installed,
   then any other package trying to Require util, might possibly grab
   math-classes instead.

Perhaps something like haskells package system would be appropriate.

  Tom