The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Given a term, is there a way to do selective zeta reduction, so that 
only certain local definitions are reduced?  For example, consider a 
term like:

  let x:=1 in let y:=2 in f x y

is there a way to do zeta reduction only on y, to end up with:

  let x:=1 in f x 2

I'm not even sure how one would pick out which local definition to 
target - perhaps by its value or type.  Even if there was just a way to 
reduce only the outermost local definition, that could perhaps be used 
to build a more general approach.

Is there anything along these lines in Coq?

-- Jonathan