The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

On Sat, 10 Jun 2006 10:39:59 -0400 "Ethan Aubin" 
<ethan.aubin AT gmail.com>
 wrote:
> Hi, Is it possible to perform a single step of delta/beta/etc
> reduction via a tactic? Is the evaulation order of the conversion
> tactics (or CiC) specified?  Also, whats the best forum to ask novice
> questions? Thanks - Ethan

You have cbv and lazy which perform "small" reduction steps, but
generally not atomic steps. See the online documentation ->
tactic index, look for "cbv". I am not sure there is something closer
to what you are looking.

You can give arguments to delta to target a particular constant.

Hope this helps,

Pierre