X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;fp=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;h=b5a194951abd8871f5b2a4a640ccd3f2c08350f3;hb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;hp=abe61f38769871fb007e1e53c83e686dabfd7dc4;hpb=68eea268e230d7eb12cdc416ead471a86a4bb5e4;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index abe61f387..b5a194951 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -31,10 +31,10 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; -type sort_kind = [ `Prop | `Set | `Type | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] val string_of_sort: sort_kind -> string -val sort_of_string: string -> sort_kind +(*val sort_of_string: string -> sort_kind*) val sort_of_sort: Cic.sort -> sort_kind val acic_object_of_cic_object :