The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 7 Jul 2012 19:20:34 -0400,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> 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

Not sure if it is useful, but Records accepts definitions as fields.

For instance you can define:

Record foo (x : nat) :=
{ n : nat
; from_param := x + n
; o : nat
; spec : o = from_param
}.

Which is the same as
Record foo (x : nat) :=
{ n : nat
; o : nat
; spec : o = x + n
}.
Definition from_param x (r:foo x) := x + (n r).

But in the first example, "from_param" is folded in the definition of
the record, which may be what you whish.

If I well remember, it was not documented in 8.3, and I didn't checked
if it was in 8.4.