The Coq mailing list

[t x <txrev319 AT gmail.com>]

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?