From 40ee96a0392fbc0945c48b5b134aa1be36f86225 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 May 2016 14:10:20 +0200
Subject: Univ: Use loc even if there are more unbound levels

---
 engine/uState.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 73b2318515..2fb64cd6e5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -263,13 +263,11 @@ let universe_context ?names ctx =
        if not (Univ.LSet.is_empty left) then
          let n = Univ.LSet.cardinal left in
          let loc =
-           if n == 1 then
-             try
-               let info =
-                 Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
-               Option.default Loc.ghost info.uloc
-             with Not_found -> Loc.ghost
-           else Loc.ghost
+           try
+             let info =
+               Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+             Option.default Loc.ghost info.uloc
+           with Not_found -> Loc.ghost
          in
            user_err_loc (loc, "universe_context",
 			(str(CString.plural n "Universe") ++ spc () ++
-- 
cgit v1.2.3