diff options
| author | Hugo Herbelin | 2019-08-29 11:34:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-08-29 11:34:22 +0200 |
| commit | 8b1dc61c0885bb5a51bc4740255584c2a00d7511 (patch) | |
| tree | d7d793794ec97976d3339f21d722ee29d8e941df /lib | |
| parent | 1ab00ddd8fa6ca5428c7f6ff56de0562bcb4ca1f (diff) | |
| parent | 61f4df8b5b974302e8b48bcf271aa68757db69fe (diff) | |
Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup flags.
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.mli | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 4 |
3 files changed, 1 insertions, 7 deletions
diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 60c8fb4449..b241fdc6cc 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t val aux_file_name_for : string -> string val start_aux_file : aux_file:string -> v_file:string -> unit -val stop_aux_file : unit -> unit +val stop_aux_file : unit -> unit val recording : unit -> bool val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 190de5853d..f09dc48f5d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let record_aux_file = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 1c96796220..185a5f8425 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,10 +31,6 @@ (** Command-line flags *) -(** Set by coqtop to tell the kernel to output to the aux file; will - be eventually removed by cleanups such as PR#1103 *) -val record_aux_file : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool |