The Coq mailing list

[roconnor AT theorem.ca]

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.''