The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le dimanche 26 septembre 2010 à 14:01 +0200, Michael a écrit :

> Getting here gives me the Error: The reference truncate_real_to_int was not
> found in the current environment. I guess I'd just have to "Require Export"
> some more, but how do I find out what?

The symbol should be in jessie_why, which you are already importing. So
I guess that the version of Why you are using is not compatible (too
old?) with the version of Jessie you are using. Perhaps it is a
packaging issue.

Best regards,

Guillaume