The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe [Axiom] and [Parameter] are nearly absolute synonyms, and [Parameters] differs from [Parameter] only in the warnings that it emits (and is otherwise identical to [Parameter]).  I've never used [Conjecture], so I'm not sure about that.  (Looking at the code, [Axiom] prints "prfax" in the .glob file, while [Parameter] prints "defax", but there is essentially no other difference.)

I believe [Variable] and [Hypothesis] are absolute synonyms, and [Variables] and [Hypotheses] are absolute synonyms.

Feel free to submit a bug report or pull request about improving the documentation.

On Sat, Mar 21, 2015 at 12:44 PM, Frederic Chyzak <frederic.chyzak AT inria.fr> wrote:

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