X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=b039b7e5ba0405ea1ca507916eff07935c7a131c;hb=67dd51c6c9ceb0186490033d77769d49404964ac;hp=c5bbfff78b34d658e347e817d84c0857d8b0aae5;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index c5bbfff78..b039b7e5b 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -30,7 +30,7 @@ type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
-  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
+  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
   | `CProp -> "CProp"
 
 let sort_of_sort = function
@@ -49,11 +49,11 @@ let xxx_add h k v =
 let xxx_type_of_aux' m c t =
  let res,_ =
    try
-    CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
+    CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph
    with
    | CicTypeChecker.AssertFailure _
    | CicTypeChecker.TypeCheckerFailure _ ->
-       Cic.Sort Cic.Prop, CicUniv.empty_ugraph
+       Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph
   in
  res
 ;;