From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 13:05:27 +0000 (+0000)
Subject: Pretty printing of Cic.Implict (Some `Hole) is now "%"
X-Git-Tag: PRE_GETTER_STORAGE~93
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=67f1b69e9b6fe608e94657f914ec79edbfe7469c;p=helm.git

Pretty printing of Cic.Implict (Some `Hole) is now "%"
---

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