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

NAME

coqmktop - The Coq Proof Assistant user-tactics linker

CONTENTS

Synopsis
Description
Options
See Also

SYNOPSIS

coqmktop [ options ] files

DESCRIPTION

coqmktop builds a new Coq toplevel extended with user-tactics. files are the Objective Caml object or library files (i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. The linker produces an executable Coq toplevel which can be called directly or through coqc(1), using the -image option.

OPTIONS

-h Help. List the available options.

-srcdir dir
  Specify where the Coq source files are

-o exec-file
  Specify the name of the resulting toplevel

-opt Compile in native code

-full Link high level tactics

-top Build Coq on a ocaml toplevel (incompatible with -opt)

-R dir Specify recursively directories for Ocaml

-v8 Link with V8 grammar

SEE ALSO

coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(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.