Bug#818331: aac-tactics: FTBFS: constructor vcons (in type vT) expects 2 arguments

2016-03-19 Thread Martin Michlmayr 
* Mehdi Dogguy  [2016-03-19 09:57]:
> This looks like a duplicate of #813459.

Yes, I must have missed that, sorry.

-- 
Martin Michlmayr
Linux for HPE Helion, Hewlett Packard Enterprise

Bug#818331: aac-tactics: FTBFS: constructor vcons (in type vT) expects 2 arguments

2016-03-19 Thread Mehdi Dogguy 
Control: forcemerge 813459 818331

Hi,

On 16/03/2016 02:13, Martin Michlmayr wrote:
> Package: aac-tactics
> Version: 0.4-5
> Severity: serious
> 
> This package fails to build in unstable:
> 
>> sbuild (Debian sbuild) 0.68.0 (15 Jan 2016) on dl580gen9-02.hlinux
> ...
>> make[4]: Entering directory '/<>'
>> "coqc"  -q -opt -R "." AAC_tactics   AAC
>> File "./AAC.v", line 497, characters 8-20:
>> Error: The constructor vcons (in type vT) expects 2 arguments.
>> Makefile.coq:424: recipe for target 'AAC.vo' failed
>> make[4]: *** [AAC.vo] Error 1
>> make[4]: Leaving directory '/<>'
> 

This looks like a duplicate of #813459.

Regards,

-- 
Mehdi

Bug#818331: aac-tactics: FTBFS: constructor vcons (in type vT) expects 2 arguments

2016-03-15 Thread Martin Michlmayr 
Package: aac-tactics
Version: 0.4-5
Severity: serious

This package fails to build in unstable:

> sbuild (Debian sbuild) 0.68.0 (15 Jan 2016) on dl580gen9-02.hlinux
...
> make[4]: Entering directory '/<>'
> "coqc"  -q -opt -R "." AAC_tactics   AAC
> File "./AAC.v", line 497, characters 8-20:
> Error: The constructor vcons (in type vT) expects 2 arguments.
> Makefile.coq:424: recipe for target 'AAC.vo' failed
> make[4]: *** [AAC.vo] Error 1
> make[4]: Leaving directory '/<>'

-- 
Martin Michlmayr
Linux for HPE Helion, Hewlett Packard Enterprise