From 237b569dd6539fc1730dbd1dda29f83e24ef8d0c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
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')

diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v
index 43acb7bb48..29ee148733 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