coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] unfold _ in _ ?

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: [Coq-Club] unfold _ in _ ?
Date: Wed, 25 Feb 2015 15:56:22 -0500

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.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

[Coq-Club] unfold _ in _ ?, Vladimir Voevodsky, 02/25/2015
- Re: [Coq-Club] unfold _ in _ ?, Beta Ziliani, 02/25/2015
- Re: [Coq-Club] unfold _ in _ ?, Jonathan Leivent, 02/25/2015