Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello Enrico,

On 08/05/2013 07:36 PM, Enrico Tassi wrote:
> On Mon, Aug 05, 2013 at 07:26:54PM +0200, Erik Martin-Dorel wrote:
> > 2) I also tested the static compilation, and once the plug-in has been
> > compiled with Coq 8.4pl2, I get the error
> > > bin/ssrcoq -q  -I src -R theories Ssreflect   -compile theories/ssrmatching
> > > Error: cannot guess a path for Coq libraries; please use -coqlib option
>
> Can you confirm you configure coq with the -local flag?

Yes I confirm: I configured coq with flags -local -opt

Kind regards,

Erik

--
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
Tel : +33 4 92 38 79 76 (bureau F123)
Mobile : 06 87 53 69 03


http://erik.martin-dorel.org/