X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=b8ae1602c8c853510ee58302afb370a0ebcc6524;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=abb1b86f37f00295883bacedf9d5fd18cb974edc;hpb=c7619e91ca47d2551e08d0dbfc6aaa66de7eca63;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index abb1b86f3..b8ae1602c 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,7 +85,8 @@ let rec pp t l =
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
-         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+         | C.Type _ -> "Type"
+         (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 	 | C.CProp -> "CProp" 
        )
     | C.Implicit _ -> "?"