From fb0c2d365cc8921e21efbec521168dba10b69bcd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Jun 2014 20:24:35 +0200
Subject: Compute the trace of a universe inconsistency only when explicitly
 required by the printing options (i.e. when "Print Universes" is set).

---
 kernel/univ.ml        | 6 +++++-
 lib/flags.ml          | 2 ++
 lib/flags.mli         | 1 +
 pretyping/detyping.ml | 2 +-
 4 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index c459a742ef..5b4b120bdf 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -989,12 +989,16 @@ let get_explanation strict g arcu arcv =
     let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
     (** Reset all the touched arcs. *)
     let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
-    Some (List.rev c)
+    List.rev c
   with e ->
     (** Unlikely event: fatal error or signal *)
     let () = cleanup_universes g in
     raise e
 
+let get_explanation strict g arcu arcv =
+  if !Flags.univ_print then Some (get_explanation strict g arcu arcv)
+  else None
+
 type fast_order = FastEQ | FastLT | FastLE | FastNLE
 
 let fast_compare_neq strict g arcu arcv =
diff --git a/lib/flags.ml b/lib/flags.ml
index 530617b0cb..9ef32989c8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -81,6 +81,8 @@ let raw_print = ref false
 
 let record_print = ref true
 
+let univ_print = ref false
+
 let we_are_parsing = ref false
 
 (* Compatibility mode *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 57e31394e6..2ce78d8827 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -44,6 +44,7 @@ val load_proofs : load_proofs ref
 
 val raw_print : bool ref
 val record_print : bool ref
+val univ_print : bool ref
 
 type compat_version = V8_2 | V8_3 | V8_4 | Current
 val compat_version : compat_version ref
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 390c3a82e1..a7a8bf5bed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -29,7 +29,7 @@ open Decl_kinds
 let dl = Loc.ghost
 
 (** Should we keep details of universes during detyping ? *)
-let print_universes = ref false
+let print_universes = Flags.univ_print
 
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
-- 
cgit v1.2.3