| C.Type ([(`Type|`CProp),u] as univ) ->
if is_declared univ then (C.Type [`Succ, u])
else
+ let universes = !universes in
raise (UntypableSort (lazy ("undeclared universe " ^
NUri.string_of_uri u ^ "\ndeclared ones are: " ^
- String.concat ", " (List.map NUri.string_of_uri !universes)
+ String.concat ", " (List.map NUri.string_of_uri universes)
)))
| C.Type t ->
raise (AssertFailure (lazy (