12.8 Module specification
Given a Coq vernacular file, the gallina filter extracts its specification (inductive types declarations, definitions, type of lemmas and theorems), removing the proofs parts of the file. The Coq file file.v gives birth to the specification file file.g (where the suffix .g stands for Gallina).See the man page of gallina for more details and options.