From d40ad33ad3d075c5dd74b6a67131683b0ebe32d6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Oct 2009 11:19:03 +0000 Subject: [PATCH] Error message fixed (dereferencing must be done eagerly, not when the error is actually printed!) --- helm/software/components/ng_kernel/nCicEnvironment.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 ( -- 2.39.2