aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
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