X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=8172b47f7ac92ce9a9fdee3fada7775cc048c84d;hb=41bb791af5cba55838dae8307339aea5098c4e2d;hp=152cdd19835f602987b34bb762987cdb481b3d09;hpb=d0420e9a7ddc25d98e04f6c24046c02b57cb8cc4;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 152cdd198..8172b47f7 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,10 +85,10 @@ 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 -> "?"
+    | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)