]> matita.cs.unibo.it Git - helm.git/commitdiff
Error message fixed (dereferencing must be done eagerly, not when the error is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Oct 2009 11:19:03 +0000 (11:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Oct 2009 11:19:03 +0000 (11:19 +0000)
actually printed!)

helm/software/components/ng_kernel/nCicEnvironment.ml

index 912dad936ed5e042569a7a95004ebd6f1c3c4c2b..df1fc849d6ffaa199b56c559a4ee9369d6c6ae7d 100644 (file)
@@ -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 (