coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Matej Košík <mail AT matej-kosik.net>
To: Kenneth Roe <kendroe AT hotmail.com>, "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:14:53 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
Ironport-phdr: 9a23:6Kq8ZhEIwzZ/6afnBqfGUJ1GYnF86YWxBRYc798ds5kLTJ75osiwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWapAQfERTnNAdzOv+9WsuL15z2hM2s9ofsYwRUiX/4SPsyaUzu9USC/vUR1KhvLKA81huBmHxFM7BVyGVkP1Wetxb7+sK5/Zol+CNV7bZpvcVHSODxe7kyZb1eFjUvdW4vroW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKklyLmu+g1+y5ouM6+GbU9WDCK6q53RR2tiyAcNj1/9mzL3J8jxJlHqQ6s8kQsi7XfZ5uYYb8kJvvQ
Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

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.

Attachment: signature.asc
Description: OpenPGP digital signature

[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