coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Avoiding some unfold with simpl

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Avoiding some unfold with simpl
Date: Tue, 26 Oct 2010 13:36:53 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=eli+VY+dX1KV9151TNo7fxJosPTuiPrxxuj+GwwpS2KVxz20mEBBhtdm2eAMhHv8d9 Hho5g1QOrI6L9soo2vnG7b34O8pR5888/2msQ6sNcWJABGghuJaf/Vy7Z0ws7b8s9hOH kVAF2ZkuBG1QkJnexxHBeMw//1lL3Q5A/5L6M=

Dear list

I would like to declare some definitions to be not unfoldable by
simpl, so that it doesn't go "too far".
I tried "Opaque myconst.", but then, even unfold fails.

I there a better way?

Thanks

Alexandre Pilkiewicz

[Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl, Adam Chlipala
  - Re: [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
    - Re: [Coq-Club] Avoiding some unfold with simpl, Mathieu Boespflug
- Re: [Coq-Club] Avoiding some unfold with simpl, Lauri Alanko
  - Re: [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz