aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/options.ml12
-rw-r--r--lib/options.mli2
2 files changed, 9 insertions, 5 deletions
diff --git a/lib/options.ml b/lib/options.ml
index 80b4631233..afa419d679 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -10,6 +10,11 @@
open Util
+let with_option o f x =
+ let old = !o in o:=true;
+ try let r = f x in o := old; r
+ with e -> o := old; raise e
+
let boot = ref false
let batch_mode = ref false
@@ -26,6 +31,8 @@ let xml_export = ref false
let dont_load_proofs = ref false
+let raw_print = ref false
+
let v7 =
let transl = array_exists ((=) "-translate") Sys.argv in
let v7 = array_exists ((=) "-v7") Sys.argv in
@@ -66,11 +73,6 @@ let silently f x =
let if_silent f x = if !silent then f x
let if_verbose f x = if not !silent then f x
-let with_option o f x =
- let old = !o in o:=true;
- try let r = f x in o := old; r
- with e -> o := old; raise e
-
(* The number of printed hypothesis in a goal *)
let print_hyps_limit = ref (None : int option)
diff --git a/lib/options.mli b/lib/options.mli
index 41e8dea844..395efc649a 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -25,6 +25,8 @@ val xml_export : bool ref
val dont_load_proofs : bool ref
+val raw_print : bool ref
+
val v7 : bool ref
val v7_only : bool ref