The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Kenneth Roe 
<kendroe AT hotmail.com>
 writes:

> Actually, I figured out this error.  It turns out the files in the
> .mllib file need to be ordered by dependencies.

Indeed.

> Env

Be extremely careful here! You are using a module name in your plugin
that clashes with a module defined by Coq `Env`. This is bad, and even
if it works in practice, could create all kind of undefined behaviors.

You have to choices to solve this problem:

- rename your env module such that its name becomes globally unique
  [wrt Coq and all the plugins you may ever load]

- Move to 8.6 and use a .mlpack file, so your plugin's modules will be
  "packed" and these kind of conflicts are avoided.

E.