From 3bcca0aecb368a723d247d1f8b2348790bc87035 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 17 Jan 2015 20:17:17 +0530
Subject: Univs: proper printing of global and local universe names (only
 printing functions touched in the kernel).

---
 test-suite/bugs/closed/3392.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/bugs/closed/3392.v')

diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v
index 43acb7bb4..29ee14873 100644
--- a/test-suite/bugs/closed/3392.v
+++ b/test-suite/bugs/closed/3392.v
@@ -25,7 +25,7 @@ Proof.
   refine (isequiv_adjointify (functor_forall f g)
                              (functor_forall (f^-1)
                                              (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y
-                             )) _ _);
+                             )) _ _); 
   intros h.
   - abstract (
         apply path_forall; intros b; unfold functor_forall;
-- 
cgit v1.2.3