Imported Upstream version 8.5~beta1+dfsg

1 files changed, 108 insertions, 47 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index f6d98ba5..c8e7f7af 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,47 +8,116 @@
 
 let with_option o f x =
   let old = !o in o:=true;
-  try let r = f x in o := old; r
-  with reraise -> o := old; raise reraise
+   try let r = f x in if !o = true then o := old; r
+   with reraise ->
+     let reraise = Backtrace.add_backtrace reraise in
+     let () = o := old in
+     Exninfo.iraise reraise
+
+let with_options ol f x =
+  let vl = List.map (!) ol in
+  let () = List.iter (fun r -> r := true) ol in
+  try
+    let r = f x in
+    let () = List.iter2 (:=) ol vl in r
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    let () = List.iter2 (:=) ol vl in
+    Exninfo.iraise reraise
 
 let without_option o f x =
   let old = !o in o:=false;
+  try let r = f x in if !o = false then o := old; r
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    let () = o := old in
+    Exninfo.iraise reraise
+
+let with_extra_values o l f x =
+  let old = !o in o:=old@l;
   try let r = f x in o := old; r
-  with reraise -> o := old; raise reraise
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    let () = o := old in
+    Exninfo.iraise reraise
 
 let boot = ref false
-
+let load_init = ref true
 let batch_mode = ref false
 
-let debug = ref false
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+let compilation_mode = ref BuildVo
+
+type async_proofs = APoff | APonLazy | APon
+let async_proofs_mode = ref APoff
+type cache = Force
+let async_proofs_cache = ref None
+let async_proofs_n_workers = ref 1
+let async_proofs_n_tacworkers = ref 2
+let async_proofs_private_flags = ref None
+let async_proofs_full = ref false
+let async_proofs_never_reopen_branch = ref false
+let async_proofs_flags_for_workers = ref []
+let async_proofs_worker_id = ref "master"
+type priority = Low | High
+let async_proofs_worker_priority = ref Low
+let string_of_priority = function Low -> "low" | High -> "high"
+let priority_of_string = function
+  | "low" -> Low
+  | "high" -> High
+  | _ -> raise (Invalid_argument "priority_of_string")
+
+let async_proofs_is_worker () =
+  !async_proofs_worker_id <> "master"
+let async_proofs_is_master () =
+  !async_proofs_mode = APon && !async_proofs_worker_id = "master"
 
-let print_emacs = ref false
+let debug = ref false
+let in_debugger = ref false
+let in_toplevel = ref false
 
-let term_quality = ref false
+let profile = false
 
-let xml_export = ref false
+let print_emacs = ref false
+let coqtop_ui = ref false
 
-type load_proofs = Force | Lazy | Dont
+let ide_slave = ref false
+let ideslave_coqtop_flags = ref None
 
-let load_proofs = ref Lazy
+let time = ref false
 
 let raw_print = ref false
 
 let record_print = ref true
 
+let univ_print = ref false
+
+let we_are_parsing = ref false
+
 (* Compatibility mode *)
 
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_2 | V8_3 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | Current
+
 let compat_version = ref Current
-let version_strictly_greater v = !compat_version > v
+
+let version_strictly_greater v = match !compat_version, v with
+| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
+| V8_3, (V8_3 | V8_4 | Current) -> false
+| V8_4, (V8_4 | Current) -> false
+| Current, Current -> false
+| V8_3, V8_2 -> true
+| V8_4, (V8_2 | V8_3) -> true
+| Current, (V8_2 | V8_3 | V8_4) -> true
+
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
+  | V8_4 -> "8.4"
   | Current -> "current"
 
 (* Translate *)
@@ -73,7 +142,23 @@ 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 universe_polymorphism = ref false
+let make_universe_polymorphism b = universe_polymorphism := b
+let is_universe_polymorphism () = !universe_polymorphism
+
+let local_polymorphic_flag = ref None
+let use_polymorphic_flag () = 
+  match !local_polymorphic_flag with 
+  | Some p -> local_polymorphic_flag := None; p
+  | None -> is_universe_polymorphism ()
+let make_polymorphic_flag b =
+  local_polymorphic_flag := Some b
+
+(** [program_mode] tells that Program mode has been activated, either
+    globally via [Set Program] or locally via the Program command prefix. *)
+
+let program_mode = ref false
+let is_program_mode () = !program_mode
 
 let warn = ref true
 let make_warn flag = warn := flag;  ()
@@ -85,28 +170,8 @@ 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
 
-(* A list of the areas of the system where "unsafe" operation
- * has been requested *)
-
-module Stringset = Set.Make(struct type t = string let compare = compare end)
-
-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 external tools *)
 
-let subst_command_placeholder s t =
-  let buff = Buffer.create (String.length s + String.length t) in
-  let i = ref 0 in
-  while (!i < String.length s) do
-    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
-    then (Buffer.add_string buff t;incr i)
-    else Buffer.add_char buff s.[!i];
-    incr i
-  done;
-  Buffer.contents buff
-
 let browser_cmd_fmt =
  try
   let coq_netscape_remote_var = "COQREMOTEBROWSER" in
@@ -122,21 +187,9 @@ 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 (
-  (* same as Envars.coqroot, but copied here because of dependencies *)
-  Filename.dirname
-    (canonical_path_name (Filename.dirname Sys.executable_name))
-)
+let coqlib = ref "(not initialized yet)"
 
 (* Options for changing camlbin (used by coqmktop) *)
 let camlbin_spec = ref false
@@ -152,3 +205,11 @@ let default_inline_level = 100
 let inline_level = ref default_inline_level
 let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
+
+(* Disabling native code compilation for conversion and normalization *)
+let no_native_compiler = ref Coq_config.no_native_compiler
+
+(* Print the mod uid associated to a vo file by the native compiler *)
+let print_mod_uid = ref false
+
+let tactic_context_compat = ref false