X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=b0e7d64ed31be5f58e6c3c095b29eac6a845ee70;hb=b59af8af91b819bfac1137e3a4d37c35c6f38f1e;hp=5c5bd71fff473b8522256c633a0fa7c5e9546c74;hpb=3eca59409abc3dc4a3c4b07752282fb47e2a5c30;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 5c5bd71ff..b0e7d64ed 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -69,7 +69,7 @@ let rec pp t l = (match get_nth l n with Some (C.Name s) -> s | Some C.Anonymous -> "__" ^ string_of_int n - | _ -> raise CicPpInternalError + | None -> "_hidden_" ^ string_of_int n ) with NotEnoughElements -> string_of_int (List.length l - n) @@ -88,7 +88,7 @@ let rec pp t l = | C.Type -> "Type" | C.CProp -> "CProp" ) - | C.Implicit -> "?" + | C.Implicit _ -> "?" | C.Prod (b,s,t) -> (match b with C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)