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

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d9c669ed5..d11dc5766 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -89,6 +89,7 @@ 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