The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 04/03/2016 17:14, Igor Zhirkov wrote:
> The Coq reference manual says that using Variable keyword is equivalent
> to Local Parameter, but I failed to find any explanation of the Local
> Parameter itself.

The Parameter command is documented as being an alias for Axiom and,
Local Axiom is indeed described in the Axiom section:

https://coq.inria.fr/refman/Reference-Manual003.html#hevea_default34

PMP

Attachment: signature.asc
Description: OpenPGP digital signature