Hello Stéphane, 2009/8/18 Stéphane Glondu <steph@glondu.net>: > It looks like it's coq-float. It depends on Coq ABI, which is > $COQVERSION-$OCAMLVERSION. It must be recompiled before why. Thank you for the explanation. Michael Biena has triggered a recompilation of the packages in the proper order. Yours, d.