X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.mli;h=c3cf56e889974b56bd9c03695c3ce8dd4ed140f1;hb=b58b7f9f3fdf8d66522b31828faa5bfa588c31b8;hp=b63a585e6bab0aafaa6cfc8faba6bace779f3cf6;hpb=c465c17581bf606e0330cbd89b238279c184ad35;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli index b63a585e6..c3cf56e88 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 ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe] val string_of_sort: sort_kind -> string (*val sort_of_string: string -> sort_kind*)