The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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.