Ssreflect Users Discussion List

["John Wiegley" <>]

I'm using the SSReflect library, and when I extract my program to Haskell, I
get the following warning.  Perhaps there are some definitions in the library
which should be made transparent?

    Warning: The extraction is currently set to bypass opacity,
    the following opaque constant bodies have been accessed :
     andP eqP eqnP idP iffP inj_eqAxiom pair_eqP val_eqP.

Thanks, John