The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/18/2014 03:36 PM, Daniel Schepler wrote:
> > 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 -> ...".

Oh - I see what you are saying now.  The issue is the conflicting 
possible sources of proof irrelevance in the proof of B - either as an 
axiom on its own (as in A), or as proven through classical facts - and 
hence not axiomatic.

You scared me for a moment there.

-- Jonathan