X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=c595c6d7dfc03bb9564908be5293994a5249215d;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=cd5ab3ace32f14593d9b85f29a3f52ff34955173;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;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 _ -> "?"