X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.mli;h=0bf874e86fd45ae6bab8564d1ea98ed3b271b59e;hb=2bcf927f58bac034b8758173cdbd16cb7475de36;hp=9182ad618794b21c5fa6b6c86d3ca5d74ab21dba;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli index 9182ad618..0bf874e86 100644 --- a/helm/software/components/cic_acic/cic2acic.mli +++ b/helm/software/components/cic_acic/cic2acic.mli @@ -31,7 +31,7 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; -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] val string_of_sort: sort_kind -> string (*val sort_of_string: string -> sort_kind*)