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=4f686da443ef71b1cc2a4a869aa855f4b3a71a80;hb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;hp=b34d34342981c17c50436f97c2c12338bf63a71e;hpb=cfaa4ba59014ccb6046a2a672e97a5e88d7d2946;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index b34d34342..4f686da44 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.mli
+++ b/helm/ocaml/cic_omdoc/cic2acic.mli
@@ -54,3 +54,12 @@ val acic_object_of_cic_object :
     (Cic.id, anntypes) Hashtbl.t *        (* ids_to_inner_types *)
     (Cic.id, Cic.conjecture) Hashtbl.t *  (* ids_to_conjectures *)
     (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
+
+val asequent_of_sequent :
+  Cic.metasenv ->                         (* metasenv *)
+   Cic.conjecture ->                      (* conjecture *)
+    Cic.annconjecture *                   (* annotated conjecture *)
+    (Cic.id, Cic.term) Hashtbl.t *        (* ids_to_terms *)
+    (Cic.id, Cic.id option) Hashtbl.t *   (* ids_to_father_ids *)
+    (Cic.id, string) Hashtbl.t *          (* ids_to_inner_sorts *)
+    (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)