The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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