From 05843c92e0fe96f09c7c4cb3d55376b99e6ea16b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 17 Mar 2019 18:32:26 +0100
Subject: Use local universe names when printing universe inconsistency

---
 vernac/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 047bdd2b61..1c58abc2fd 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -308,7 +308,7 @@ let explain_unification_error env sigma p1 p2 = function
      | UnifUnivInconsistency p ->
         if !Constrextern.print_universes then
 	  [str "universe inconsistency: " ++
-          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
+          Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p]
 	else
           [str "universe inconsistency"]
      | CannotSolveConstraint ((pb,env,t,u),e) ->
-- 
cgit v1.2.3