diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 39 |
1 files changed, 26 insertions, 13 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 6b68a8f2..470cf81f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r @@ -25,19 +23,22 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false -let print_emacs_safechar = ref false let term_quality = ref false let xml_export = ref false -let dont_load_proofs = ref false +type load_proofs = Force | Lazy | Dont + +let load_proofs = ref Lazy let raw_print = ref false +let record_print = ref true + (* Compatibility mode *) -type compat_version = V8_2 +type compat_version = V8_2 | V8_3 let compat_version = ref None let version_strictly_greater v = match !compat_version with None -> true | Some v' -> v'>v @@ -86,12 +87,6 @@ let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set -(* Flags for the virtual machine *) - -let boxed_definitions = ref true -let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - (* Flags for external tools *) let subst_command_placeholder s t = @@ -120,9 +115,21 @@ let is_standard_doc_url url = url = Coq_config.wwwrefman || url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) +(* same as in System, but copied here because of dependencies *) +let canonical_path_name p = + let current = Sys.getcwd () in + Sys.chdir p; + let result = Sys.getcwd () in + Sys.chdir current; + result + (* Options for changing coqlib *) let coqlib_spec = ref false -let coqlib = ref Coq_config.coqlib +let coqlib = ref ( + (* same as Envars.coqroot, but copied here because of dependencies *) + Filename.dirname + (canonical_path_name (Filename.dirname Sys.executable_name)) +) (* Options for changing camlbin (used by coqmktop) *) let camlbin_spec = ref false @@ -132,3 +139,9 @@ let camlbin = ref Coq_config.camlbin let camlp4bin_spec = ref false let camlp4bin = ref Coq_config.camlp4bin +(* Level of inlining during a functor application *) + +let default_inline_level = 100 +let inline_level = ref default_inline_level +let set_inline_level = (:=) inline_level +let get_inline_level () = !inline_level |