The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

I'm curious about the interaction of this feature with extraction.
In the example you gave:

> Fixpoint f (x:nat) : nat := let y := f x in 0.

extraction to Ocaml yields:

  let rec f x = 0

This suggests that the body of a recursive function is
normalized before extraction.  But this example:

  Fixpoint g (x:nat) : nat := 
    let z1 := x * x in
    let z2 := z1 * z1 in
    let z3 := z2 * z2 in
    let z4 := g z3 * g z3 in
    z3 * z3.

yields the following Ocaml:

  let rec g x =
    let z1 = mult x x in
    let z2 = mult z1 z1 in 
    let z3 = mult z2 z2 in 
    mult z3 z3

so obviously, something more clever is happening.

-Greg