X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic2OCic.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic2OCic.ml;h=5f8279d7e67cb3660652e392b882a49cc4fa63a7;hb=28f01bb2d0e5f1b3f180b0b478267d2beb06a5fe;hp=d9edb1100c7d45340f97a907353decc2fc345c6d;hpb=6b843ebfba2ed19d2bf7a564a9d2fc92da880169;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index d9edb1100..5f8279d7e 100644
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -37,7 +37,7 @@ let convert_term uri n_fl t =
  | NCic.Sort (NCic.Type u) when
     (* BUG HERE: I should use NCicEnvironment.universe_eq, but I do not
        want to add this recursion between the modules *)
-    (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort Cic.CProp 
+    (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
  | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
  | NCic.Implicit _ -> assert false
  | NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) ->