X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=876f6a261670692977b2cb34d1d50726bcdfcffc;hb=6c384ea974e161acb78eaa7fcea87950f801fd0b;hp=f16c1a98cfb0a90214bd2b3fe4474f1f7682d1d2;hpb=f233a527ff4233ae9dc948550b0b5adef16696e0;p=helm.git

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 ->