X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=d11dc576695cb54c7229e7c12828bdd00a4f8b99;hb=0f3081bec320860fbe2208e4d3314629e12a320f;hp=b8ae1602c8c853510ee58302afb370a0ebcc6524;hpb=d450cacb49707a71fe93489a1bf64db4689612d6;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index b8ae1602c..d11dc5766 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -89,13 +89,14 @@ let rec pp t l =
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 	 | C.CProp -> "CProp" 
        )
+    | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           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) ->