X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=695b2e5319f61df33cdd05115c4058c2cf94adbd;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=c19561d355821bfffa6fa7fceffeb11ef0a299cd;hpb=498898aa5d4525d979fe5564c180ab75f6483c99;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c19561d35..695b2e531 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -391,7 +391,12 @@ let rec typeof ~subst ~metasenv context term =
         with Failure _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
-    | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+    | C.Sort (C.Type ([false,u] as univ)) ->
+       if NCicEnvironment.is_declared univ then
+        C.Sort (C.Type [true, u])
+       else
+        raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+         NUri.string_of_uri u)))
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
           NCicPp.ppterm ~subst ~metasenv ~context t)))