From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 15:13:47 +0000 (+0000)
Subject: use universe rank instead of Type0
X-Git-Tag: make_still_working~5355
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4164d93a5e0ac9c6d66dde4c88b3302b01fda743;p=helm.git

use universe rank instead of Type0
---

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index f16c1a98c..876f6a261 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -462,7 +462,8 @@ let convert_term uri t =
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
     | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
-    | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] 
+    | Cic.Sort (Cic.Type u) -> 
+          NCic.Sort (NCic.Type (CicUniv.get_rank u)),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l ->