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).

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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