X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.mli;h=4526521fbd0e6d00f6e57d0b0eb6f05ab8636c09;hb=cbb7f68d7d012f385e74d466f0bce7881d9eb71c;hp=c3cf56e889974b56bd9c03695c3ce8dd4ed140f1;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index c3cf56e88..4526521fb 100644
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -59,3 +59,10 @@ val asequent_of_sequent :
     (Cic.id, Cic.hypothesis) Hashtbl.t)    (* ids_to_hypotheses *)
 
 val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj
+
+val acic_term_of_cic_term :
+  ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
+  Cic.context -> Cic.term ->               (* term and context *)
+   Cic.annterm *                            (* annotated term *)
+    (Cic.id, sort_kind) Hashtbl.t *         (* ids_to_inner_sorts *)
+    (Cic.id, anntypes) Hashtbl.t            (* ids_to_inner_types *)