]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/acic2Ast.mli
version 0.7.1
[helm.git] / helm / ocaml / cic_transformations / acic2Ast.mli
index 3db26629adc9b857867ab7ad5e64a467a23375ad..411057cffbd8d7b1470d325358710492c5bef713 100644 (file)
  *)
 
 val ast_of_acic :
-  (Cic.id, string) Hashtbl.t -> (* id -> sort *)
-  (Cic.id, string) Hashtbl.t -> (* id -> uri *)
+  (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> (* id -> sort *)
 (*
+  (Cic.id, string) Hashtbl.t -> (* id -> uri *)
   (string,
    Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) ->
      CicAst.term)
    Hashtbl.t ->
 *)
-    Cic.annterm -> CicAst.term * (Cic.id, string) Hashtbl.t
+    Cic.annterm ->
+      CicAst.term * (Cic.id, string) Hashtbl.t  (* ast, id -> uri *)