diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 11:05:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 11:05:00 +0100 |
| commit | b233d38a7a6a3e73f093c5c5ec00f1a7582e7668 (patch) | |
| tree | 3467207f621885afcaf131295d5516dfe38ae53b /toplevel | |
| parent | e687dd9b1ee68b4ae00461a379a5207d6187a6d1 (diff) | |
| parent | 5bf25dfce23da1cee04b1c886e026f0dbc902c9c (diff) | |
Merge PR #11075: load .vo when .vos is missing + misc vos changes
Reviewed-by: gares
Reviewed-by: silene
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, |