Re: Bug#813596: coq-float and why cannot be built with Coq 8.5 (Bugs #813596 and #815684)

[Nicolas Braud-Santoni <nicolas@braud-santoni.eu>]

Control: tag -1 upstream

On Sat, Jul 23, 2016 at 08:35:15PM +0200, Ralf Treinen wrote:
> 
> Why also does not compile with the current vesion of why3. I talked 
> to why upstream about this a few days ago. There will be a new upstream
> release of why soon which will fix this. I suspect this will also 
> fix compilation whith coq-8.5.
> 
> I also asked him whether it stills makes sense to maintain a package
> for why and was told that yes, since why3 does not yet support
> interfaces to frama-c and krakakoa. 
> 
> I don't know about coq-float, though.


That's great news!

Thanks a lot  :)