The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hmm, 

  then I retract my point, thanks for the correction :) My analysis 
only applies to let '_ := f x in 0, which really disappears (and 
Eval compute in f 0 terminates).

Best,
— Matthieu

Le 12 févr. 2014 à 15:30, Bruno Barras 
<bruno.barras AT inria.fr>
 a écrit :

> On 12/02/2014 10:47, Matthieu Sozeau wrote:
>> Hi,
>> 
>>   Let me make my point again: what you see is not what you get ([Print f])!
>> The definition of f that goes into the kernel does not contain the let
>> binding anymore,
> 
> Matthieu,
> 
> All the versions of Coq I've used do keep this let, including today's 
> trunk, and die on Eval compute (f 0).
> 
> Extraction is smart, but not enough to deal with
> 
> Definition K (x:nat) (y:nat) := x.
> Program Fixpoint f (x:nat) : nat :=
>  K 0 (f x).
> Extraction f.
> (* let rec f x = k O (f x) *)
> 
> Bruno.
> 
>