Compute the trace of a universe inconsistency only when explicitly required

by the printing options (i.e. when "Print Universes" is set).

1 files changed, 5 insertions, 1 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index c459a742e..5b4b120bd 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 =