The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks for that reassurance.

I'm pretty sure now that what I observed was NOT a bug in Print Assumptions. 

Instead, I was being stupid and thinking that a proof was using a lemma when it was not.

Sorry.

-- Abhishek

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

On Fri, Jan 10, 2014 at 1:19 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

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/