]> matita.cs.unibo.it Git - helm.git/commitdiff
workaround for some Set/Type problems
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 16:50:10 +0000 (16:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 18 Apr 2008 16:50:10 +0000 (16:50 +0000)
helm/software/components/ng_kernel/oCic2NCic.ml

index 4aaeb414c4d8330e70b6dc4cd3d224981b254f66..320df7c9f201b2aaa0445ca39400e6e9416b755b 100644 (file)
@@ -497,7 +497,7 @@ 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)),[] 
+          NCic.Sort (NCic.Type (CicUniv.get_rank u+1)),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l ->