The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

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