diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ccompile.ml | 7 | ||||
| -rw-r--r-- | toplevel/coqcargs.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 3cbbf3d186..3c198dc600 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -150,8 +150,11 @@ let compile opts copts ~echo ~f_in ~f_out = Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); - (* Produce an empty .vos file when producing a .vo in standard mode *) - if mode = BuildVo then create_empty_file (long_f_dot_out ^ "s"); + (* Produce an empty .vos file and an empty .vok file when producing a .vo in standard mode *) + if mode = BuildVo then begin + create_empty_file (long_f_dot_out ^ "s"); + create_empty_file (long_f_dot_out ^ "k"); + end; (* Produce an empty .vok file when in -vok mode *) if mode = BuildVok then create_empty_file (long_f_dot_out); Dumpglob.end_dump_glob () diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index 677a3f2e48..18c51f4229 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -10,7 +10,7 @@ (** Compilation modes: - BuildVo : process statements and proofs (standard compilation), - and also output an empty .vos file + and also output an empty .vos file and .vok file - BuildVio : process statements, delay proofs in futures - Vio2Vo : load delayed proofs and process them - BuildVos : process statements, and discard proofs, |