The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I think Print Assumption is conservative: if there is an axiom you will see some axioms. However, as it happens, modules make things complicated. The version I first wrote basically ignored module, and in some circumstances reported way to many axioms. I think it was something about modules with abstract interfaces. Anyway, Pierre Letouzey wrote a significantly more extensive version which deals with modules. It may still raise too many axioms (non-axioms may mask other axioms), but not as often.

Anyway, I believe you can trust the "Closed under the global context" assertion (otherwise you have found a real bug).

Arnaud

On 9 January 2014 21:09, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Suppose I prove some theorem(say T) and then Print Assumptions T says:

"Closed under the global context".

Can I then be  sure that the proof does not (possibly indirectly) depend on some

unproved assumptions(Axioms, Admits)?

I'm not sure if I was dreaming, but I think that once Print Assumptions said that on a lemma

whose proof used other lemmas whose proofs had admits in them.

I can't replicate that problem today.

-- Abhishek

http://www.cs.cornell.edu/~aa755/