The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 08.07.2012 01:20, schrieb Jason Gross:
> Hi,
> Is there a way to make a constant opaque or transparent within a 
> tactic?  Relatedly, is there a way to state that a constant should 
> usually be opaque, unless its first few arguments match a specific 
> pattern?
>
> The context is that I've moved some [Record] fields to parameters, so 
> that I get sort-polymorphism, but I want to pretend that these things 
> are record fields, so that I can build tactics that match on them and 
> so that the "fields that are really parameters" carry along the 
> information of what record they come from.  So I generally want these 
> things to be opaque, so that [simpl] and [hnf] don't unfold them, but 
> I sometimes need to see inside them.  (Currently, there seems to be a 
> theorem that I can only [eapply] if I make these transparent.)  So I 
> either want to tune how opaque these constants are, and/or I want to 
> be able to flip opaqueness back and forth inside of tactics.
>
> Thanks!
>
> -Jason

No, but I'm sure that you can Hack arround it by having a second 
definition that you prove to be equal to the first one, then you make 
the second one opaque.

Definition plusopaque x y := x + y.
Lemma pluseq : forall x y, plusopaque x y = x + y.
reflexivity. Qed.

Opaque plusopaque.