The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I was under the impression from section 2.4.2 of the reference manual, where it says:

"After closing of the section, the local declarations (variables and local definitions) get discharged, meaning that they stop being visible and that all global objects defined in the section are generalized with respect to the variables and local definitions they each depended on in the section."

that this meant that any global objects would omit from their definitions section variables and local definitions on which they do not depend.  However, I am finding that this isn't happening, at least not in the naive way I am thinking about dependencies.  I have a case where a section variable is counted as part of a definition (a proof) by this dependency analysis - and so appears as an argument to the definition after the section ends - but the definition (and its proof) still works if I just delete that section variable completely.

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?

I was experimenting with sections because I realized I could perhaps use the PG "store goal" command plus some emacs hacking to automate the out-of-line abstraction of a subgoal into a separate proof - by taking that stored goal and turning it into a section where the hypotheses are variables and the consequent is the one (non-variable) definition in the section.  But of course, some of those variables may not be needed to prove the subgoal - and that's where I was hoping that the end-of-section dependency analysis would help me out.  But it's not.

-- Jonathan