The Coq mailing list

[roconnor AT theorem.ca]

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.

Lemma foo1 : X -> nat.
unfold X.
tauto.
Qed.

Opaque X.

Lemma foo2 : X -> nat.
(* unfold X. doesn't work *)
apply foo1.
Qed.

But now when foo.v is imported

(* File: bar.v *)

Require Export foo.

Lemma bar1 : X -> nat.
unfold X. (* Now works *)
tauto.
Qed.

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