The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list,

There seems to be a difference of opacity between a definition that is
made opaque, and a Qed at the end of a lemma:

<<<
Definition false_opaque := True.
Global Opaque false_opaque.
About false_opaque.
(*false_opaque : Prop

false_opaque is basically transparent but considered opaque for reduction
Expands to: Constant Top.false_opaque*)

Goal false_opaque.
constructor.
Qed.

Definition true_opaque:Prop. exact True. Qed.
About true_opaque.
(*true_opaque : Prop

true_opaque is opaque
Expands to: Constant Top.true_opaque*)

Goal true_opaque.
constructor. (* Error: Not an inductive product. *)
>>>

Is there a good reason for that? And if not, what would be a
"RealOpaque" command, to avoid ma opaque constant to be "basically
transparent"?

Cheers

Alexandre