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

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d9c669ed570e318173056744488fa88b58ab4876..d11dc576695cb54c7229e7c12828bdd00a4f8b99 100644 (file)
--- 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