aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 11:11:50 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 11:11:50 +0100
commit073b92396a68be30f77c80960a58ca562bb01f49 (patch)
treed2ad366f28624196ebfe9c1eadf595dcb490fcdc /lib
parentc047ecce6e4dba33df69a53a9e168999676c65db (diff)
parented18f926e4695acc730218925ca156abe56ba5fc (diff)
Merge PR #6753: [toplevel] Make toplevel state into a record.
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli1
2 files changed, 0 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 01361dad5..415e4399a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -56,10 +56,8 @@ let in_toplevel = ref false
let profile = false
let ide_slave = ref false
-let ideslave_coqtop_flags = ref None
let raw_print = ref false
-
let univ_print = ref false
let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 33d281798..c82410f07 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -33,7 +33,6 @@ val profile : bool
(* -ide_slave: printing will be more verbose, will affect stm caching *)
val ide_slave : bool ref
-val ideslave_coqtop_flags : string option ref
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref