aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-12 18:35:21 +0200
committerMaxime Dénès2017-04-12 18:35:21 +0200
commita5c150a6a7fa980c5850aa247e62d02e29773235 (patch)
treee8f9a6211c3626d80d8427887bf181d10a3476f9 /lib/flags.ml
parenta74d64efb554e9fd57b8ec97fca7677033cc4fc4 (diff)
parentb63b9a86b09856262b5b7bb2b3bb01f704032d41 (diff)
Merge PR#441: Port Toplevel to the Stm API
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml9
1 files changed, 0 insertions, 9 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 5b080151cd..d87d9e7295 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,8 +86,6 @@ let in_toplevel = ref false
let profile = false
let print_emacs = ref false
-let coqtop_ui = ref false
-
let xml_export = ref false
let ide_slave = ref false
@@ -97,7 +95,6 @@ let time = ref false
let raw_print = ref false
-let record_print = ref true
let univ_print = ref false
@@ -183,12 +180,6 @@ let warn = ref true
let make_warn flag = warn := flag; ()
let if_warn f x = if !warn then f x
-(* The number of printed hypothesis in a goal *)
-
-let print_hyps_limit = ref (None : int option)
-let set_print_hyps_limit n = print_hyps_limit := n
-let print_hyps_limit () = !print_hyps_limit
-
(* Flags for external tools *)
let browser_cmd_fmt =