Error message fixed (dereferencing must be done eagerly, not when the error is

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 912dad936ed5e042569a7a95004ebd6f1c3c4c2b..df1fc849d6ffaa199b56c559a4ee9369d6c6ae7d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -146,9 +146,10 @@ let typeof_sort = function
   | 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 (