David MENTRE a écrit : > I'm not quite sure of the blocking point. Is it "coq"? "coq-float"? A > synchronization is needed or just a re-compilation? I would appreciate > any help. It looks like it's coq-float. It depends on Coq ABI, which is $COQVERSION-$OCAMLVERSION. It must be recompiled before why. Cheers, -- Stéphane