summaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml27
1 files changed, 24 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 928912e6..12d25c54 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: flags.ml 11801 2009-01-18 20:11:41Z herbelin $ i*)
+(*i $Id$ i*)
let with_option o f x =
let old = !o in o:=true;
@@ -37,6 +37,14 @@ let raw_print = ref false
let unicode_syntax = ref false
+(* Compatibility mode *)
+
+type compat_version = V8_2
+let compat_version = ref None
+let version_strictly_greater v =
+ match !compat_version with None -> true | Some v' -> v'>v
+let version_less_or_equal v = not (version_strictly_greater v)
+
(* Translate *)
let beautify = ref false
let make_beautify f = beautify := f
@@ -55,6 +63,10 @@ let verbosely f x = without_option silent f x
let if_silent f x = if !silent then f x
let if_verbose f x = if not !silent then f x
+let auto_intros = ref true
+let make_auto_intros flag = auto_intros := flag
+let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
+
let hash_cons_proofs = ref true
let warn = ref true
@@ -80,8 +92,8 @@ let is_unsafe s = Stringset.mem s !unsafe_set
let boxed_definitions = ref true
let set_boxed_definitions b = boxed_definitions := b
-let boxed_definitions _ = !boxed_definitions
-
+let boxed_definitions _ = !boxed_definitions
+
(* Flags for external tools *)
let subst_command_placeholder s t =
@@ -102,6 +114,15 @@ let browser_cmd_fmt =
with
Not_found -> Coq_config.browser
+let is_standard_doc_url url =
+ let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
+ let wwwprefix = "http://coq.inria.fr/" in
+ let n = String.length wwwprefix in
+ let n' = String.length Coq_config.wwwrefman in
+ url = Coq_config.localwwwrefman ||
+ url = Coq_config.wwwrefman ||
+ url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
+
(* Options for changing coqlib *)
let coqlib_spec = ref false
let coqlib = ref Coq_config.coqlib