coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Carlos.SIMPSON" <carlos AT math1.unice.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Re:Opaque
- Date: Tue, 22 Oct 2002 11:12:53 -0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Re:Opaque, Carlos.SIMPSON
Archive powered by MhonArc 2.6.16.