The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Try adding `open Ltac_plugin` at the top of your file.

Maxime.

On 11/04/2017 04:52 PM, Kenneth Roe wrote:
> It looks like I'm getting closer.  My file compiles.  However, I get the
> following error:
> 
> File "./src/Theory.v", line 74, characters 0-28:
> 
> *Error:*
> 
> while loading /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs:
> 
> error loading shared library:
> dlopen(/Users/kendroe/FDS/engine/plugin/src/thepack.cmxs, 138): Symbol
> not found: _camlTacenv
> 
>   Referenced from: /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs
> 
>   Expected in: flat namespace
> 
>  in /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs
> 
> 
> 
> I discovered the cause of this undefined symbol is this macro:
> 
> TACTIC EXTEND AR2
> 
> | ["arewrite"] -> [Stuff.arewrite]
> 
> END
> 
> 
> When I comment it out, the resulting module loads.  What do I need to
> include or change?
> 
>                  - Ken
> 
> ------------------------------------------------------------------------
> *From:* Matej Košík 
> <mail AT matej-kosik.net>
> *Sent:* Saturday, November 4, 2017 6:30 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 14:10, Kenneth Roe wrote:
>> Didn't work.
>> 
>> Does someone have a sample project that uses "VERNAC COMMAND EXTEND" (and 
>> also "TACTIC EXTEND" or what ever it became) for Coq 8.7?
> 
> The attached demo exercises some of those mechanisms.
> (Compiles with the "v8.7" branch of Coq).
> 
> Let me know what you think.
> 
> ---
> 
> Matej