diff options
Diffstat (limited to 'engine/uState.ml')
-rw-r--r-- | engine/uState.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 73b231851..2fb64cd6e 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 () ++ |