The Coq mailing list

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

On Feb 11, 2014, at 6:54 PM, Mitchell Wand 
<wand AT ccs.neu.edu>
 wrote:

> Is this a CBN vs. CBV issue?

Yes.  I'd argue that if termination checking is allowing for:

  Fixpoint f (x:nat) : nat := let z := f(x) in 0

then the language isn't confluent, and so it's easy to run into
problems when reduction is done one way, and extraction + evaluation
is done another.

But I suspect Pierre was smart enough to cover the bases here
and it's not really a problem.  I was just hoping someone knew
what, exactly, is going on.

-Greg