Bug#815684: why can't be built from source

[Matthias Klose <doko@debian.org>]

Package: src:why
Version: 2.24-3
Severity: serious

Tags: sid

[Mehdi asked me to file RC issues ... I saw these while working on some 
transitions in Ubuntu, and trying to keep creduce in unstable/testing]

why doesn't work with the coq in unstable, and coq-float doesn't work with the 
coq in unstable. Saw that coq-float is optional, tried to build it:

  coqc  -R lib/coq Why lib/coq/WhyInt.v
  coqc  -R lib/coq Why lib/coq/WhyArrays.v
  coqc  -R lib/coq Why lib/coq/WhyBool.v
  coqc  -R lib/coq Why lib/coq/WhyTuples.v
  File "./lib/coq/WhyTuples.v", line 26, characters 23-26:
  Error: Cannot infer the implicit parameter A of fst whose type is "Type".
  Makefile:974: recipe for target 'lib/coq/WhyTuples.vo' failed
  make[1]: *** [lib/coq/WhyTuples.vo] Error 1

Then I just removed the libwhy-coq package so that why builds again. For that I 
had to disable the testsuite, relying on coq.