From ff4d0d98ab0e0e81bd1acf9a7bf4b64913834911 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 14:10:03 +0200
Subject: Remove Print Universe directive.

---
 theories/Init/Logic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 375495c888..50f853f0e0 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -370,7 +370,7 @@ Module EqNotations.
 End EqNotations.
 
 Import EqNotations.
-Set Printing Universes.
+
 Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
 Proof.
 intros.
-- 
cgit v1.2.3