X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=d9c669ed570e318173056744488fa88b58ab4876;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;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..d9c669ed5 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 _ -> "?"
@@ -94,7 +95,7 @@ let rec pp t l =
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
         | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
        )
-    | C.Cast (v,t) -> pp v l
+    | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.LetIn (b,s,t) ->