]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2acic.mli
Dead code/files removed.
[helm.git] / helm / ocaml / cic_omdoc / cic2acic.mli
index 2dd0a2f319652c0995b5230369ed582596df8aff..ff75618f84f2b41413c54e002decde233bf5a0c3 100644 (file)
@@ -37,19 +37,6 @@ val string_of_sort: sort_kind -> string
 val sort_of_string: string -> sort_kind
 val sort_of_sort: Cic.sort -> sort_kind
 
-val acic_of_cic_context' :
-  int ref ->                              (* seed *)
-  (Cic.id, Cic.term) Hashtbl.t ->         (* ids_to_terms *)
-  (Cic.id, Cic.id option) Hashtbl.t ->    (* ids_to_father_ids *)
-  (Cic.id, sort_kind) Hashtbl.t ->        (* ids_to_inner_sorts *)
-  (Cic.id, anntypes) Hashtbl.t ->         (* ids_to_inner_types *)
-  Cic.metasenv ->                         (* metasenv *)
-  Cic.context ->                          (* context *)
-  Cic.id list ->                          (* idrefs *)
-  Cic.term ->                             (* term *)
-  Cic.term option ->                      (* expected type *)
-  Cic.annterm                             (* annotated term *)
-
 val acic_object_of_cic_object :
   ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
   Cic.obj ->                              (* object *)