The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I do not think there is a way to have Ltac change those flags.  However, the command

Arguments foo : simpl never.

will cause [simpl] not to expand [foo].  You will still be able to [unfold foo], and [compute] will unfold it as well.

-Jason

On Friday, July 12, 2013, t x wrote:

Hi,

  Consider this minimal failure case: https://gist.github.com/anonymous/1e3d9502fa56ca742b00

  Question:

    Is there anyway to have a Ltac change Transparent/Opaque flags? (For example, the following does not compile:

Ltac solve_foo :=

  Transparent foo;

  match goal with ...

  How I'm running into this problem:

  In my proofs, I want certain functions to be "barriers" -- to have "simpl" NOT unfold them, so that (1) I can pattern match on them and (2) there are different "levels" to the proof

  Now, having pattern matched on them, I want to solve them using specific tactics -- and for this I do need to be able to unfold them.

  Thus, is there a way for ltac to locally control whether terms are Opaque/Transparent?