]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2acic.mli
added universes
[helm.git] / helm / ocaml / cic_omdoc / cic2acic.mli
index abe61f38769871fb007e1e53c83e686dabfd7dc4..b5a194951abd8871f5b2a4a640ccd3f2c08350f3 100644 (file)
@@ -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 :