X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;h=b5a194951abd8871f5b2a4a640ccd3f2c08350f3;hb=00bba19fcd102e03db20f273740047b77a84be80;hp=ff75618f84f2b41413c54e002decde233bf5a0c3;hpb=18ab6500105671c07f65430be5c899732fc101c3;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index ff75618f8..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 :
@@ -57,3 +57,4 @@ val asequent_of_sequent :
     (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
     (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
 
+val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj