X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8;hb=4514417676056e0be6cc481a931e70a627882867;hp=9ad05dc926725e75b9ca287ebc4b8e3324ae4a9e;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index 9ad05dc92..3285dcc15 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -25,13 +25,14 @@ (* $Id$ *) -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string] let string_of_sort = function | `Prop -> "Prop" | `Set -> "Set" | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) | `NType s -> "Type[" ^ s ^ "]" + | `NCProp s -> "CProp[" ^ s ^ "]" | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)