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 f16c1a98cfb0a90214bd2b3fe4474f1f7682d1d2..876f6a261670692977b2cb34d1d50726bcdfcffc 100644 (file)
--- 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 ->