From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 lib/flags.ml | 39 ++++++++++++++++++++++++++-------------
 1 file changed, 26 insertions(+), 13 deletions(-)

(limited to 'lib/flags.ml')

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
-- 
cgit v1.2.3