diff options
| author | charguer | 2019-11-08 11:06:10 +0100 |
|---|---|---|
| committer | charguer | 2019-11-20 12:02:00 +0100 |
| commit | 5bf25dfce23da1cee04b1c886e026f0dbc902c9c (patch) | |
| tree | 44258f30e5965dcfc1e316c4bd4812698dcf7777 /toplevel | |
| parent | 64ddd9ac0c34e560a0640297e2e23b6aaf074810 (diff) | |
From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
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, |