What does V stand for in the Coq file extension?

Question

Is .v for verification? validation? vamanos?

Why not use a .coq extension?

Answer 1

There are two languages in Coq:

1. Gallina, the term language, and
2. an administration language called the Vernacular,

in particular:

This chapter describes Gallina, the specification language of Coq. It allows developing mathematical theories and proofs of specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in theories is described in Section 1.2. The language of commands, called The Vernacular is described in section 1.3.

The corresponding file extensions are:

1. .g for Gallina files, which result from .v files after removing the proofs (see also this message)
2. .v for Vernacular files.