diff options
| author | Hugo Herbelin | 2019-05-08 21:28:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:15:15 +0200 |
| commit | 63a953ddc0db1ec1bf101ed6afdf9262d0d9f355 (patch) | |
| tree | b8b12986afa3c31115c57c66e69429047ce6667f /library/library.mli | |
| parent | d452f359566ec6593aad564acb281f5a49dd931a (diff) | |
Ensuring suffix of file to compile also for -vio2vo checking.
We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).
For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.
Incidentally, this avoids the non-recommended Loadpath.locate_file.
Diffstat (limited to 'library/library.mli')
| -rw-r--r-- | library/library.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.mli b/library/library.mli index a976be0184..390299bf56 100644 --- a/library/library.mli +++ b/library/library.mli @@ -46,7 +46,7 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) |