diff options
| author | Hugo Herbelin | 2019-05-07 09:11:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:37:50 +0200 |
| commit | d4bb58a66ebaa771216524c070a090e60d4fb7a9 (patch) | |
| tree | 4099cb6427c2aec543c16ebbff632009e742292c | |
| parent | 44a5643416fbb0e224cf0031f176bd859ef2faf5 (diff) | |
Coqc: Ensure exclusiveness of options -quick and -vio2vo.
| -rw-r--r-- | toplevel/coqcargs.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index c3f099869c..0ccd68613f 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -82,6 +82,14 @@ let set_vio_checking_j opts opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 +let set_compilation_mode opts mode = + match opts.compilation_mode with + | BuildVo -> { opts with compilation_mode = mode } + | mode' when mode <> mode' -> + prerr_endline "Options -quick and -vio2vo are exclusive"; + exit 1 + | _ -> opts + let get_task_list s = List.map (fun s -> try int_of_string s @@ -145,7 +153,7 @@ let parse arglist : t = | "-o" -> { oval with compilation_output_name = Some (next ()) } | "-quick" -> - { oval with compilation_mode = BuildVio } + set_compilation_mode oval BuildVio | "-check-vio-tasks" -> let tno = get_task_list (next ()) in let tfile = next () in @@ -164,7 +172,7 @@ let parse arglist : t = | "-vio2vo" -> let oval = add_compile ~echo:false oval (next ()) in - { oval with compilation_mode = Vio2Vo } + set_compilation_mode oval Vio2Vo | "-outputstate" -> set_outputstate oval (next ()) |