coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

From: Kenneth Roe <kendroe AT hotmail.com>
To: Matej Košík <mail AT matej-kosik.net>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7
Date: Sat, 4 Nov 2017 23:18:45 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM04-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:0rNr2hN/83mCJMPniyYl6mtUPXoX/o7sNwtQ0KIMzox0KP35rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6ms3EwnyNz1WIRZwGcaGis2208i38oHeYUBLgyG8YvV0IQng6U2bvc4PxIBmN6wZyx3To3IOdf4cjTdjIkvWlBLh7O+x+oRi+mJeoaRy2dRHVPDZcqI+QKBYRA4hPihh58DtuQPEQCOP4WcZW2QS1BFPBl6Wv1nBQp7tv36i5aJG0y6AMJiuQA==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Both are indeed there.

- Ken

From: Matej Košík <mail AT matej-kosik.net>
Sent: Saturday, November 4, 2017 3:14 PM
To: Kenneth Roe; coq-club AT inria.fr
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

On 11/04/17 22:37, Kenneth Roe wrote:
> I have
>
> DECLARE PLUGIN "theplug"
>
>
> at the top of the file. Changing it to
>
> Declare ML Module "theplug"
>
>
> generates a syntax error from the preprocessor.

That is not surprising at all.

This:

DECLARE PLUGIN "theplug"

only makes sense in an Ocaml source code whereas:
(i.e. in *.ml4 file)

Declare ML Module "theplug".

only makes sense in *.v file.
(provided that the object file of your plugin is "theplug.cmo" or "theplugin.cma")

Each of those two commands has different purpose.

[Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
- Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Hugo Herbelin, 11/04/2017
  - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
    - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
      - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Maxime Dénès, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/05/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/05/2017