The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Thanks, I would not have guessed that I would one day:
- be unable to play a game in Coq due to performance concerns, and see
them fixed in the very next version of it
- feel the need for Emacs' "electric terminator" option

On Sun, Mar 30, 2014 at 5:43 PM, Laurent Théry 
<Laurent.Thery AT inria.fr>
 wrote:
> On 03/30/2014 06:08 PM, AUGER Cédric wrote:
>>
>> Le Sun, 30 Mar 2014 01:14:35 +0100,
>> Laurent Théry 
>> <Laurent.Thery AT inria.fr>
>>  a écrit :
>>
>> For a small increase in performances, it would have been better to
>> remember only the exponent, instead of the whole natural number (unary
>> integers are not very good wrt Coq memory when they can become quite
>> big).
>
> Thanks! I have updated the file using N instead of nat .
>
> http://www-sop.inria.fr/marelle/Laurent.Thery/T2048.v
>
> --
> Laurent
>