diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-19 07:41:09 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-19 07:41:09 +0200 |
| commit | 802366bdf00adf3849499f43ba07ee726da0668a (patch) | |
| tree | a5d0c160d98a9f414dc670df47ac5840b86506ea /lib/aux_file.mli | |
| parent | f7fb1918619fcef384d4aa84938246de67c707fa (diff) | |
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
Diffstat (limited to 'lib/aux_file.mli')
| -rw-r--r-- | lib/aux_file.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 127827ab6..86e322b71 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -17,7 +17,8 @@ module H : Map.S with type key = int * int module M : Map.S with type key = string val contents : aux_file -> string M.t H.t -val start_aux_file_for : string -> unit +val aux_file_name_for : string -> string +val start_aux_file : aux_file:string -> v_file:string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool |