Skip to Content.
Sympa Menu

ssreflect - Re: Ssreflect, coercions, and module import

Subject: Ssreflect Users Discussion List

List archive

Re: Ssreflect, coercions, and module import


Chronological Thread 
  • From: Guillaume Melquiond <>
  • To:
  • Subject: Re: Ssreflect, coercions, and module import
  • Date: Sun, 13 May 2012 11:16:16 +0200

Le dimanche 13 mai 2012 à 10:38 +0200, Enrico Tassi a écrit :
> On Sun, May 13, 2012 at 09:13:40AM +0200, Guillaume Melquiond wrote:
> > 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.
>
> I don't get exactly your problem, but does it vanish with that?
>
>
> http://patch-tracker.debian.org/patch/series/view/ssreflect/1.3pl2-3/0002-Activated-option-Automatic-Coercions-Import.patch
>
> If so I'll make pl release with the fix. But I was waiting for a patch
> from Cyril...

Please don't include this "fix". As it happens, the issue was with my
system: my version of ssreflect was actually already using this patch,
unbeknown to me. Once I reverted it, things started to work fine again.
Sorry for the noise.

Best regards,

Guillaume




Archive powered by MHonArc 2.6.18.

Top of Page