coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Kenneth Roe <kendroe AT hotmail.com>
Subject: Re: [Coq-Club] Sample Coq 8.7 ML plugin
Date: Mon, 30 Oct 2017 08:23:54 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:vZlYYRScVLZ4q6wQ/kvFFLvW8Npsv+yvbD5Q0YIujvd0So/mwa64ZBKN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBDgyP4ardvJj23qx/Qv48Ym88qCas3zBbVojNyfOkekWBlI16JmBvU5sCs+Zdi92JbvPd3pOBaVqCvRa08Q/R6ETIpezQ3+cvknRzbTE6U+WBaVX8ZxEkbSzPZ5Q33C8+i+hDxsfBwjWzDZZX7

Hi,

I recently ported this one to at least compile on 8.7:
https://github.com/ppedrot/coq-string-ident

; 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

[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