coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?
Date: Wed, 29 Mar 2017 20:56:51 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f175.google.com
Ironport-phdr: 9a23:jFjO8xAMJ2ZTf+eRigfuUyQJP3N1i/DPJgcQr6AfoPdwSPv8ocbcNUDSrc9gkEXOFd2CrakV16yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBC/AOPf1fr4n7ulAArAG+BQ63BOP01zRFgX320rch0+QmFwHG0xYgH9UVsHTPqNj4L6gSUeWvw6nJyTXPde9Z2TD46IXRdB0qvP+CXbV1ccXLyEkvERvIjk+OpozkMTOZzOENs2yD4+p6S+2vimAnpBltoje12sgslojJiZ4Oylze8CV5xIA4LsC7Rk5jedOoDodcuiWAO4Z1Qs4uWX9ktDs7x7EcpJK2figHxZI6zBDFcfOHaZKH4hf7WeaRPzh4gHVldaq6hxmo8EigzvTwVtCo0FpWtyZFnMTAu3IN2hDJ5ciHTfx9/kil2TmRzQzc9uZEIUUsmaraLZ4u3KIwm4INvUjfGiL6gkb7ga+Mekk65+Sl6v7rbqjkq5KcL4N0jxvxMqUqmsyxG+Q4NQ0OUnCZ+eumz73j+kv5QLpQjv0xianZq5TXKN8Upq68GQBV04Ij5wyjADeh1dQUhWMHI05deBKbk4jpPEnDL+z/DfemmlijjDNrx+3dMbD6GZXMLn3DkK/7crpn6k5czhAzzdFF6J5OBLEBOqG7Zkikv9vBSxQ9Lgb8l+3gEZB20p4UcWOJGK6Qdq3I5wym/OUqdsuFf4gT8BnnLOM+r6rshGQ+n1AHerKyjLMYbXm5GrJtJEDPMimkucsIDWpf5ll2d+ftklDXCTM=

Thanks! That seem to have done the trick, as long as I add it in both reif_tactics.ml and reif.ml4, and add it above the other `open`s in reif.ml4.

On Wed, Mar 29, 2017 at 5:02 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

e AT x80.org (Emilio Jesús Gallego Arias) writes:

> Did you do `open Ltac_plugin` in reif.ml, as instructed in
> `dev/doc/changes.txt` ?

s/reif.ml/reif.ml4/

I just had a look to your code, yup, that seems like the culprit, now
ltac is a plugin and you must open the packed module in every file using
ltac.

E.

[Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017
- Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
  - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
    - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017