The Coq mailing list

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

Hello Kenneth,

Kenneth Roe 
<kendroe AT hotmail.com>
 writes:

> It appears that the file intern.cmi and intern.cmo are not being
> properly loaded into the Coq environment.  How do I fix this bug?
> This is what I have in my _CoqProject file (which is sent to
> coq_makefile) to create the makefile:

You are likely missing a mllib/mlpack file.

> src/advanced_rewrite.ml4

Assuming you are using Coq 8.7 [which you should be], I suggest you add
a file to _CoqProject:

src/advanced_rewrite_plugin.mlpack

and fill out that file with the modules that should be in your
plugin. Then, you can `load advanced_rewrite_plugin` from your v file.

E.