Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re:Opaque

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re:Opaque


chronological Thread 

Perhaps a Virtual Opaque command would be in order: this
would say, keep the constant as transparent but make it so that all
tactics behave as if it
were opaque.  In that case you could keep the standard library files but
change the saving command
so that everything is saved as Virtual Opaque; theoretically the files
should then compile with no problem
(except maybe time).
???
---Carlos





Archive powered by MhonArc 2.6.16.

Top of Page