aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli4
1 files changed, 0 insertions, 4 deletions
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