Ssreflect Users Discussion List

[Guillaume Melquiond <>]

Hi,

I'm encountering a strange issue with 8.3pl4 and 1.3pl2 and I wonder if
this rings a bell to someone. I don't remember having this issue with
earlier versions, but I can't say for sure whether it comes from Coq,
ssreflect, or my system.

Require Import Rineq Qcanon.
Require Import ssreflect.
Print Coercions.
(* this neg nonneg nonpos nonzero pos sigT_of_sig
sig_of_sigT *)

Require Import Rineq Qcanon ssreflect.
Print Coercions.
(* sigT_of_sig
sig_of_sigT *)

As you can, if ssreflect happens to be imported on the same line as
other libraries, the coercions of those libraries vanish into thin air.

Best regards,

Guillaume