X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=8e7cb7c21226de2ac743f3ef0548f7a7b16f1011;hb=e2381427bca733bd36a099002fa8b7140f7a20d0;hp=d50b67c8e9bc0838cb338b1155599bdcaead6f95;hpb=fa9700ea545ddaed416fdabb9d9fb410ef528e97;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index d50b67c8e..8e7cb7c21 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -15,6 +15,13 @@ module Ref = NReference
 
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
+let mk_type n = 
+  if n = 0 then
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+  else
+     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+;;
+
 (* porcatissima *)
 type reference = Ref of NUri.uri * NReference.spec
 let reference_of_ouri u indinfo =
@@ -616,8 +623,8 @@ let convert_term uri t =
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
     | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
     | Cic.Sort (Cic.Type u) -> 
-          NCic.Sort (NCic.Type (CicUniv.get_rank u)),[] 
-    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
+          NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
+    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l -> 
         let l, fixpoints =