Subject: Ssreflect Users Discussion List
List archive
- 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
- Ssreflect, coercions, and module import, Guillaume Melquiond, 05/13/2012
- Re: Ssreflect, coercions, and module import, Enrico Tassi, 05/13/2012
- Re: Ssreflect, coercions, and module import, Guillaume Melquiond, 05/13/2012
- Re: Ssreflect, coercions, and module import, Enrico Tassi, 05/13/2012
Archive powered by MHonArc 2.6.18.