The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I cannot test here, but isn’t there any distinction on whether or not the term defined in section is opaque?

2014-06-25 8:29 GMT+02:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 24/06/2014 23:53, Jonathan wrote:

Could someone describe in more detail what is supposed to go on at the
end of a section with regard to this dependency analysis?  I might be
seeing a bug, or I might just not understand what is involved in a
dependency according to this analysis.  Is it perhaps that some tactics
involved in the proof of the definition create "false" dependencies that
aren't really needed, but are still honored with respect to
end-of-section dependency analysis?

As long as the hypotheses appear in the constructed proof terms, they are actual dependencies. You can Print the proved theorems to see where they come from. Do you happen to use any automatic tactic (auto, omega, assumption, etc)? Such tactics don't try to find the minimal subset of hypotheses needed for proving a goal. And even if they were doing this extra work locally, that would not guarantee that the whole theorem would use a minimal subset of hypotheses.

Best regards,

Guillaume

--
.../Sedrikov\...