From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 17:58:08 +0200
Subject: Split off Universes functions dealing with names.

This API is a bit strange, I expect it will change at some point.
---
 vernac/explainErr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/explainErr.ml')

diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f9167f969..f68dcae26 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -55,7 +55,7 @@ let process_vernac_interp_error exn = match fst exn with
     let msg =
       if !Constrextern.print_universes then
 	str "." ++ spc() ++ 
-	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
+          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
       else
 	mt() in
     wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
-- 
cgit v1.2.3