- Changed ApplyTransformation API to return both the mathml and acic,

[helm.git] / helm / ocaml / cic_transformations / applyTransformation.mli

diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli
index 1b646aa6e9a4d3cb02522c1ec524f3fd040b42f2..f7d3d2da2c09cfa15b1e865e8ee44eba02d9bbde 100644 (file)
--- a/helm/ocaml/cic_transformations/applyTransformation.mli
+++ b/helm/ocaml/cic_transformations/applyTransformation.mli
@@ -37,16 +37,21 @@ val mml_of_cic_sequent :
  Cic.metasenv ->                          (* metasenv *)
  Cic.conjecture ->                        (* sequent *)
   Gdome.document *                            (* Math ML *)
+   (Cic.annconjecture *                       (* annsequent *)
     ((Cic.id, Cic.term) Hashtbl.t *           (* id -> term *)
      (Cic.id, Cic.id option) Hashtbl.t *      (* id -> father id *)
-     (Cic.id, Cic.hypothesis) Hashtbl.t)      (* id -> hypothesis *)
+     (Cic.id, Cic.hypothesis) Hashtbl.t *     (* id -> hypothesis *)
+     (Cic.id, string) Hashtbl.t))             (* ids_to_inner_sorts *)
 
 val mml_of_cic_object :
   UriManager.uri ->                       (* object uri *)
   Cic.obj ->                              (* uri *)
     Gdome.document *                          (* Math ML *)
+     (Cic.annobj *                            (* annobj *)
       ((Cic.id, Cic.term) Hashtbl.t *         (* id -> term *)
        (Cic.id, Cic.id option) Hashtbl.t *    (* id -> father id *)
        (Cic.id, Cic.conjecture) Hashtbl.t *   (* id -> conjecture *)
-       (Cic.id, Cic.hypothesis) Hashtbl.t)    (* id -> hypothesis *)
+       (Cic.id, Cic.hypothesis) Hashtbl.t *   (* id -> hypothesis *)
+       (Cic.id, string) Hashtbl.t *           (* ids_to_inner_sorts *)
+       (Cic.id, Cic2acic.anntypes) Hashtbl.t))(* ids_to_inner_types *)