The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi Adam

2010/10/26 Adam Chlipala 
<adam AT chlipala.net>:
>
> The only way I've found to do this is to put the definition inside a module
> with opaque signature ascription.

I don't really see the difference with Opaque.

>  You can also export from the module a
> theorem giving the equation defining the identifier; then, in cases where
> you do want reduction, you have to rewrite with that equality, rather than
> relying on the definitional equality.

That's what I'm doing, yes.

Then I tried a couple of "clever" things to simplify this usage :

First I wanted to name those renaming lemma myconst_unfold, and have a tactic

Ltac unfold' X :=
  let H = concat X "_unfold" in
  rewrite H.
where concat would be a tactic that concatenate names like fresh does,
but without the freshning. But it seems it does not exists.

Then I just wanted to put the rewriting lemma in a Rewrite base:

Hint Rewrite myconst_unfold: myconst.

and have

Ltac unfold' X := autorewrite with X.

but then I encountered what seems to be a bug of ltac (
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2417 ;)

I will continue with just rewrite.

Thanks anyway!

Alexandre