---
name: "gallina"
section: "1"
platform: "linux"
package: "coq"
version: "8.6-4"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/gallina"
---

# gallina(1)

extracts specification from Coq vernacular files

## NAME

gallina - extracts specification from Coq vernacular files

## SYNOPSIS

**gallina** \[ **-** \] \[ **-stdout** \] \[ **-nocomments** \] *file ...*

## DESCRIPTION

**gallina** takes Coq files as arguments and builds the corresponding specification files. The Coq file *foo.v* gives bearth to the specification file *foo.g.* The suffix '.g' stands for Gallina.

For that purpose, gallina removes all commands that follow a "Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof \<...\>.". It also removes every "Hint", "Syntax", "Immediate"  or "Transparent" command.

Files without the .v suffix are ignored.

## OPTIONS

- **-stdout**

  Prints the result on standard output.

- **-**

  Coq source is taken on standard input. The result is printed on standard output.

- **-nocomments**

  Comments are removed in the \*.g file.

## NOTES

Nested comments are correctly handled. In particular, every command "Save." or "Abort." in a comment is not taken into account.

## BUGS

Please report any bug to **coq@pauillac.inria.fr**