Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Why Opaque?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why Opaque?


chronological Thread 

I've spent a little time reviewing some discussion about
Opaque/Transparency problems when dealing with well-founded recursion
<http://www.google.com/search?hl=en&lr=&q=+site%3Apauillac.inria.fr+coq+opaque&btnG=Search>

But I haven't figured out why anything is Opaque at all.  In particular in
Coq 7.1 a change was made so that `` Constants declared as opaque (using
Qed) can no longer become transparent (a constant intended to be
alternatively opaque and transparent must be declared as transparent
(using Defined))''.  There must have been a reason for this.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''




Archive powered by MhonArc 2.6.16.

Top of Page