X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=58f319f4a8fae7f5a91d0e4c2f9e68370d930b8e;hb=97f61628fff4436efb7c21129327b36b897348bb;hp=1686cd3572ab57d09a255d9a47f5c6409db367bb;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 1686cd357..58f319f4a 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -114,7 +114,7 @@ let rec pp t l =
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-	 | C.CProp -> "CProp" 
+	 | C.CProp _ -> "CProp" 
        )
     | C.Implicit (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
@@ -347,7 +347,7 @@ let ppsort = function
   | Cic.Prop -> "Prop"
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
+  | Cic.CProp _ -> "CProp"
 
 
 (* MATITA NAMING CONVENTION *)