Что означает V в расширении файла Coq?

Ответ 1

В Coq есть два языка:

• Gallina, язык терминов и
• язык администрирования, называемый Vernacular,

в частности:

В этой главе описывается Галлина, язык спецификации Coq. Это позволяет разрабатывать математические теории и доказательства спецификаций программ. Теории строятся из аксиом, гипотез, параметров, лемм, теорем и определений констант, функций, предикатов и множеств. Синтаксис логических объектов, участвующих в теориях, описан в разделе 1.2. Язык команд, называемый The Vernacular, описан в разделе 1.3.

Соответствующие расширения файлов:

• .g для файлов Gallina, которые выводятся из .v файлов после удаления доказательств (см. также это сообщение)
• .v для народных файлов.

Ответ 2

В справочном руководстве они называются " vernacular file ".