The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Fri, Mar 17, 2006 at 10:41:27AM -0500, 
roconnor AT theorem.ca
 wrote:

> Why is it that when you declare something as Opaque in a module, it become
> transparent when the module is imported.  For example

> (* File: foo.v *)
> Definition X := nat.

(...)

> Opaque X.

Well, it is the documented behaviour.

 At section or module closing, a constant recovers the status it got
 at the time of its definition.

I suppose that the "Opaque/Transparent" commands were supposed to be
mainly tactic hints, and not actually change the status of the defined
object.

-- 
Lionel