The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

> While I have no opinion on this particular issue, I didn't know that Print
> Assumptions would ever print out something less than the transitive closure
> of the assumptions in certain cases (as in the typeclasses case you
> describe).  If that's true, is there some way to force Print Assumptions to
> print out the transitive closure?
>
> Otherwise, for people who are using Print Assumptions as a way to check if
> inconsistent assumptions are being used together, this could be a problem.

Print Assumptions still prints out the full transitive closure.  What
I was thinking of was something more like:

Lemma A `{ProofIrrelevance} : ...
Proof.
...
apply proof_irrelevance.
...
Qed.

Lemma B `{Classic} : ...
Proof.
...
apply classic.
...
apply A.
...
Qed.

Then "Check @A" would return "ProofIrrelevance -> ...", while "apply
A." in the proof of Lemma B would fill in
(ClassicalFacts.proof_irrevance_cci classic) as the ProofIrrelevance
argument of A, and overall "Check @B" would return "Classic -> ..."
instead of "Classic -> ProofIrrelevance -> ...".
-- 
Daniel Schepler