From 67f1b69e9b6fe608e94657f914ec79edbfe7469c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 13:05:27 +0000 Subject: [PATCH] Pretty printing of Cic.Implict (Some `Hole) is now "%" --- helm/ocaml/cic_proof_checking/cicPp.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2