X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=df1fc849d6ffaa199b56c559a4ee9369d6c6ae7d;hb=d40ad33ad3d075c5dd74b6a67131683b0ebe32d6;hp=912dad936ed5e042569a7a95004ebd6f1c3c4c2b;hpb=da0c52aa34feaacdcefdf67df433ebbc367fdbc2;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 912dad936..df1fc849d 100644
--- 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 (