The Coq mailing list

[Frederic Chyzak <frederic.chyzak AT inria.fr>]

On Sat, 2015-03-21 at 11:30 -0400, Jason Gross wrote:
> [Variable] in a module now means [Local Parameter]; change [Variable]
> to [Parameter] or [Axiom] when not in a section, and you should be
> fine.

Thank you Jason for your explanation.

I think I get it now, but, first, I was wondering how ok.v can work
differently.  There may be some improvement to do with the
documentation, then:
- [Local Parameter] is used only once in the user manual, in section
1.3.1: “Using the Variable command out of any section is equivalent to
using Local Parameter.”
- The phrase [Local Parameter] is not defined by itself.  One has to see
that [Parameter ident : term] is equivalent to [Axiom ident : term] to
extrapolate that [Local Parameter] could mean [Local Axiom].  But,
reading the text, this is just a guess.
- Section 6.11.1 explains that there are different behaviours of the
Local/Global pair, depending on what scope is implied, but this text is
general: it suggests that scopes end “at the end of the section or
module”, without listing what command is sensitive to sections, modules,
or both.
- Back to section 1.3.1, the text describing [Axiom] suggests it could
be sensitive to modules, not sections.  In particular, the description
of [Local Axiom] discusses a behaviour with respect to [Import],
therefore with respect to modules, not sections.

Are [Axiom], [Conjecture], [Parameter], and [Parameters] all absolute
synonyms, whether they occur after [Local] or not, and before [ident :
term] or [ident1 ... identn : term] or [(ident1,1 ... ident1,k1 :
term1) ... (identn,1 ... identn,kn : termn)] ?

I haven't checked all those possible choices of syntax, but if their
behaviours match, the documentation should in my opinion be rewritten in
a more symmetric way.

Frédéric