The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

Hello everyone,

In the standard library's Logic file, projection is defined as 
Opaque/with Qed:

Theorem proj2 : A /\ B -> B.
  Proof.
  destruct 1; trivial.
  Qed.

I'm wondering if there's a deep reason for not making this definition 
transparent.  (I'd like to get at the underlying computational behavior 
of proj2 to help simplify another proof.)

Thanks,
Ryan Wisnesky