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  -  COQC (1)

NAME

coqc - The Coq Proof Assistant compiler

CONTENTS

Synopsis
Description
Options
See Also

SYNOPSIS

coqc [ general Coq options ] file

DESCRIPTION

coqc is the batch compiler for the Coq Proof Assistant. The options are basically the same as coqtop(1). file.v is the vernacular file to compile. file must be formed only with the characters ‘a‘ to ‘Z‘, ‘0‘-‘9‘ or ‘_‘ and must begin with a letter. The compiler produces an object file file.vo.

For interactive use of Coq, see coqtop(1).

OPTIONS

coqc is a script that simply runs coqtop with option -compile it accepts the same options as coqtop.

-image bin
  use bin as underlying coqtop instead of the default one.

-verbose print the compiled file on the standard output.

SEE ALSO

coqtop(1), coq_makefile(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr

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


--> COQ (1) April 25, 2001

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