coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
Archive powered by MHonArc 2.6.18.