diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-27 14:10:20 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-29 11:52:52 +0200 |
| commit | 40ee96a0392fbc0945c48b5b134aa1be36f86225 (patch) | |
| tree | 7f2d28d1bfb9dfb72788b434ecada5603afecb57 /engine/uState.ml | |
| parent | 23ab6c84b3d04cc2218bf1ad935fa87396999ccd (diff) | |
Univ: Use loc even if there are more unbound levels
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 () ++ |