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 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel')

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