Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2


Chronological Thread 
  • From: e AT x80.org (Emilio Jesús Gallego Arias)
  • To: Kenneth Roe <kendroe AT hotmail.com>
  • Cc: Coq-Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2
  • Date: Mon, 11 Sep 2017 01:46:06 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
  • Ironport-phdr: 9a23:tQrCLxbaeWcNtgIoSlFTHGv/LSx+4OfEezUN459isYplN5qZpsW9bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76xXcoFx7+LQt4IPjuUs6X1pzvlrP6x5qGQAhOgjehYftIKxj++QbcsMUMhoZKKqEtzxLIpj1DfOEAlk1yIlfGkj7stp/2+4Rsu2R9vvMl9skIc6jh7b9wYrVcCDkpNCgc/szirliQHkO0+nIAXzBOwVJzCA/f4US/B8+pvw==
  • Organization: X80 Heavy Industries

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.



Archive powered by MHonArc 2.6.18.

Top of Page