X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=c595c6d7dfc03bb9564908be5293994a5249215d;hb=6719c0e318b312b51b089fea3d69d1b7103245ea;hp=cd5ab3ace32f14593d9b85f29a3f52ff34955173;hpb=28f01bb2d0e5f1b3f180b0b478267d2beb06a5fe;p=helm.git

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index cd5ab3ace..c595c6d7d 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -182,7 +182,7 @@ let rec pp ~in_type t context =
          | 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 _ -> "?"