X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=8172b47f7ac92ce9a9fdee3fada7775cc048c84d;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=b0e7d64ed31be5f58e6c3c095b29eac6a845ee70;hpb=7af6bb6e640a44489bdab79a38300cf103e45bd4;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index b0e7d64ed..8172b47f7 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -85,7 +85,7 @@ let rec pp t l = (match s with C.Prop -> "Prop" | C.Set -> "Set" - | C.Type -> "Type" + | C.Type _ -> "Type" (* TASSI: universe is not explicit *) | C.CProp -> "CProp" ) | C.Implicit _ -> "?"