From 32d372f83a7797244b4e4d4f0d5791145bc615d1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:19 +0000
Subject: No more Univ in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38fe7a1ca1..7537e7d0b8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -65,7 +65,7 @@ let print_implicits_defensive = ref true
 let print_coercions = ref false
 
 (* This forces printing universe names of Type{.} *)
-let print_universes = ref false
+let print_universes = Detyping.print_universes
 
 (* This suppresses printing of primitive tokens (e.g. numeral) and symbols *)
 let print_no_symbol = ref false
-- 
cgit v1.2.3