The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

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.

                 - Ken

---

From: Matej Košík <mail AT matej-kosik.net>
Sent: Saturday, November 4, 2017 11:46 AM
To: coq-club AT inria.fr; kendroe AT hotmail.com
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

 

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)

?