added new implementation of universes

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index d50b67c8e9bc0838cb338b1155599bdcaead6f95..8e7cb7c21226de2ac743f3ef0548f7a7b16f1011 100644 (file)
--- 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 =