GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  GALLINA (1)

NAME

gallina - extracts specification from Coq vernacular files

CONTENTS

Synopsis
Description
Options
Notes
Bugs

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

        

        

        

        

Search for    or go to Top of page |  Section 1 |  Main Index


Coq tools COQ (1) 29 March 1995

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.