coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Sample Coq 8.7 ML plugin

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Kenneth Roe <kendroe AT hotmail.com>
Cc: Ralf Jung <jung AT mpi-sws.org>, "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Sample Coq 8.7 ML plugin
Date: Mon, 30 Oct 2017 15:53:54 +0100
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:5MRPShABhxJ5UQM6euWiUyQJP3N1i/DPJgcQr6AfoPdwSP3yoMbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6lX71zMZGw3+OAxpPay1X9eK14Xkn9y1rr7eZQNFmDr1W7R/ZEG1oAPdrM4bqYtlNqM4yx+PqXxNLbd432RtcF+7j0akoMCq89Yj3iFRv/Mmv+xNSjfhN4sxSbhVAzNuGno07daq5kqLdheG+nZJCjZeqRFPGQWQqUiiBpo=
Organization: X80 Heavy Industries

Dear Kenneth,

in general the differences between 8.5 ML code and 8.7 ML code should
not be large. See dev/doc/changes for a more detailed view.

Kenneth Roe
<kendroe AT hotmail.com>
writes:

> 1) How is a .mlpack file formatted? I'm told that .mlpack replaces
> .mllib?

It should use the same format.

> 2). I see a "GEXTEND" construct at the end of the file. I assume this
> replaces "TACTIC EXTEND". What is used in place of a "VERNAC COMMAND
> EXTEND" construct?

These are different constructs, VERNAC COMMAND EXTEND should still work.

> Are there any larger projects that have been ported?

I understand that quite a few large projects have been ported, some
others are in the way. Do you have some specific project in mind?

E.

[Coq-Club] Sample Coq 8.7 ML plugin, Kenneth Roe, 10/30/2017
- Re: [Coq-Club] Sample Coq 8.7 ML plugin, Ralf Jung, 10/30/2017
  - Re: [Coq-Club] Sample Coq 8.7 ML plugin, Kenneth Roe, 10/30/2017
    - Re: [Coq-Club] Sample Coq 8.7 ML plugin, Emilio Jesús Gallego Arias, 10/30/2017