The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Thanks.  However, I still need to get some more information:

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

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?

Are there any larger projects that have been ported?

                        - Ken

---

From: Ralf Jung <jung AT mpi-sws.org>
Sent: Monday, October 30, 2017 12:23 AM
To: coq-club AT inria.fr; Kenneth Roe
Subject: Re: [Coq-Club] Sample Coq 8.7 ML plugin

 

Hi,

I recently ported this one to at least compile on 8.7:
https://eur01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fppedrot%2Fcoq-string-ident&data=02%7C01%7Ckendroe%40hotmail.com%7C9ea0220ed9574cd2cd8808d51f672fc1%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C636449450394354954&sdata=QAcW6ipGjgLS7uvG3P7o4sak9tssFNUDBdV7qxd7fro%3D&reserved=0

; Ralf

On 30.10.2017 04:41, Kenneth Roe wrote:
> I've decided to upgrade my code to Coq 8.7.  Can some one point me to a
> small sample project showing how to build an ml-plugin with Coq 8.7?
>
>            - Ken