X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.mli;h=cca20ba5f805e6837c52c960208b7a9fa71554d5;hb=1652681b5eb49332f1c78e6c26d3ae5c7253d382;hp=08e49a3439acf78e6ba72f5164fef3427b5e72e7;hpb=55ec3926f6fbb5dba13705659fe94d0db38b2666;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli
index 08e49a343..cca20ba5f 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.mli
+++ b/helm/software/components/acic_procedural/acic2Procedural.mli
@@ -23,12 +23,20 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val acic2procedural:
+val procedural_of_acic_object:
+   ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+   ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> ?info:string ->
+   GrafiteAst.inline_param list -> Cic.annobj ->
+      (Cic.annterm, Cic.annterm,
+       Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
+      GrafiteAst.statement list
+
+val procedural_of_acic_term:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
-   ?depth:int -> ?skip_thm_and_qed:bool ->
-     string -> Cic.annobj ->
+   GrafiteAst.inline_param list -> Cic.context -> Cic.annterm ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list
 
+val tex_formatter: Format.formatter option ref