The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/25/2015 03:56 PM, Vladimir Voevodsky wrote:
> Hello,
>
> is there a way to say “unfold ident" in "subexp.” as one can say “change 
> subexp with exp.” ?
>
> Of course, one can not use the word “in” here but there does not seem to be 
> any other reason not to have such a feature.
>
> Vladimir.

Does this do what you want?:

set (S:=subexp) in *.
unfold ident in (value of S).
subst S.

-- Jonathan