The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello,

Thanks a lot Maxime, this solves the issue.

Sylvain.

-------- Message transféré --------
Date : Thu, 26 Oct 2017 18:34:18 +0200
De : Maxime Dénès 
<mail AT maximedenes.fr>

Hello,

You need to add an 'open Ltac_plugin' in the files that depend on Ltac
(typically the ones containing TACTIC EXTEND macros, for example).

Hope it helps.

Maxime.

On 10/26/2017 06:17 PM, Sylvain Boulmé wrote:
> Hello everybody,
>
> I am trying to update the following plugin from v8.6 to v8.7:
>   https://github.com/VERIMAG-Polyhedra/VplTactic
>
> My updated .ml and .ml4 files compile.
> The Coq files do not seem to require an update.
>
> But, on the Coq compilation, the following line
>   Declare ML Module "vpl_plugin".
> fails with the following message (whereas everything works find in v8.6):
>
> Error:
> while loading /home/sylvain/VplTactic/src/vpl_plugin.cmxs:
> error loading shared library:
> /home/sylvain/VplTactic/src/vpl_plugin.cmxs: undefined symbol:
> camlTacinterp
>
> Do you have an hint about this issue ?
> I have no idea on how to solve this.
>
> Thanks,
>
> S.