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: coq-club AT inria.fr, kendroe AT hotmail.com
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7
Date: Sat, 4 Nov 2017 19:46:53 +0100
Authentication-results: mail2-smtp-roc.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:uOXGwBJC03OSzIUW/dmcpTZWNBhigK39O0sv0rFitYgXI/TxwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBX/vHCo0j4TBhi6cCM9ZqGsQtaT3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t0GZtcQQjZFlJ44xzQfMq3pMPe9RwDBGP1WWyjP1+sqytL1kAaFT86Yk/s9EeaDzY6k6CL9fFzUldWY4+Ju45lH4UQKT6y5EAS0tmR1SDl2AtUmiUw==
Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

Hi,

On 11/04/17 17:39, Kenneth Roe wrote:
> I got the code to compile. And the commands that I registered with "VERNAC
> COMMAND EXTEND" seem to work. However, the "arewrite" tactic that I
> registered with "TACTIC EXTEND" is not recognized. I
> get the error:
>
> *Error:*The reference arewrite was not found in the current environment.

I have a stupid question:

Did you do something like:

Declare ML Module "your_plugin".

in the *.v file you are trying to compile?
(somewhere before the position in which you are trying to use the tactic
provided by that plugin)

?

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