The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

Hello,

 Coq V7 knows about "zeta"-reduction, which is elimination of "let-in"s
 But there doesn't seem to exist any flag for this conversion (to use in
some commands like "Eval Cbv Delta [f] Zeta in <term>".

 Is this addition unnecessary or planified for the future versions ?
Pierre

-- 
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |   
351 Cours de la Liberation        |   
F-33405 TALENCE Cedex             |   
France                            |   
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran