The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Abishek,

Can you share a bit of context about your use case?

Thanks!

Maxime.

On 11/15/16 18:03, Abhishek Anand wrote:
> My understanding is that once a definition is saved with Qed, there is
> no way to make it transparent.
> Is that true?
> 
> If so, has someone written a plugin/tool to take a definition (say of X)
> with possibly opaque parts and recursively transparently duplicate those
> parts to create a new totally transparent definition (say X_t)?
> 
> Perhaps no new Coq plugin is needed -- template-coq
> <https://github.com/gmalecha/template-coq>'s `Quote Recursively` already
> reifies opaque bodies. Also, it has "Make Definition" to reflect back
> encodings of definitions. It seems possible to write Ltac/Gallina
> functions that use template-coq commands to achieve the above-mentioned
> transparentification. Am I overlooking some difficulty?
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/~aa755/>