From 802366bdf00adf3849499f43ba07ee726da0668a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 19 May 2016 07:41:09 +0200 Subject: coqc: support -o option to specify output file name The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo --- library/library.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 8f5b775d8..b9044b60d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -37,9 +37,9 @@ type seg_proofs = Term.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid located list -> unit -(** Start the compilation of a file as a library. The argument must be an - existing file on the system, and the returned path is the associated - absolute logical path of the library. *) +(** Start the compilation of a file as a library. The first argument must be + output file, and the + returned path is the associated absolute logical path of the library. *) val start_library : CUnix.physical_path -> DirPath.t (** End the compilation of a library and save it to a ".vo" file *) -- cgit v1.2.3