universes are written with the URI inside objects, this allows

[helm.git] / helm / software / components / cic_acic / cic2acic.ml

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index c2f1616be8101e93899c97a1c9d28e8c8e09c1fa..b039b7e5ba0405ea1ca507916eff07935c7a131c 100644 (file)
--- 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