/
common_compile.mli
34 lines (28 loc) · 1.84 KB
/
common_compile.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* [fatal_error msg] prints msg and exits 1 *)
val fatal_error : Pp.t -> 'a
(* [ensure ext src tgt] checks that, once stripped by ext, both [src] and
[tgt] have the same basename, and returns [tgt] with the extension.
[ext] is expected to begin with dot, eg [".v"]. *)
val ensure : ext:string -> src:string -> tgt:string -> string
(* [ensure_exists f] fails if f does not exist *)
val ensure_exists : string -> unit
(* [ensure_exists_with_prefix src tgt src_ext tgt_ext] checks that [src] exists
(if needed adding the extension) and that [tgt] exists (if needed adding the
extension) and returns [src] and [tgt] with their respective extensions.
If [tgt] is [None], then it defaults to [src] (with [tgt_ext] as extension).
[src_ext] and [tgt_ext] are expected to begin with dot, eg [".v"]. *)
val ensure_exists_with_prefix : src:string -> tgt:string option -> src_ext:string -> tgt_ext:string -> string * string
(* [chop_extension f] is like Filename.chop_extension but fail safe *)
val safe_chop_extension : string -> string
(* [ensure_no_pending_proofs ~filename] checks that no proof or obligation
is open *)
val ensure_no_pending_proofs : filename:string -> Vernacstate.t -> unit