The Coq mailing list

[Christine Paulin-Mohring <Christine.Paulin-Mohring AT inria.fr>]

Dear Ivan and Marino,

In order to check the well-formednes of fixpoint definition, Coq
expands names but only transparent names. The so-called opaque names
are considered as abstract proofs, there is no need to keep the
underlying proof object. The default in Coq is that a theorem or
lemma is opaque while a definition is transparent. But an opaque 
constant can be made transparent using the command 
Transparent WEIRD. A better solution is to replace the keywords
Lemma / Qed. in the WEIRD definition by 
Definition / Defined.

Best regards,
Christine Paulin.