X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.mli;h=9fe4130c35b74433157575280d813f6bf9b11494;hb=442f3a15d7c6afc480da02602d4d4c8db4f44c10;hp=f41f0a7a1e27ad38e1fcf5240c954c0823e1f77d;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli
index f41f0a7a1..9fe4130c3 100644
--- a/helm/software/matita/applyTransformation.mli
+++ b/helm/software/matita/applyTransformation.mli
@@ -47,7 +47,8 @@ val mml_of_cic_sequent:
 val nmml_of_cic_sequent:
  NCic.metasenv -> NCic.substitution ->          (* metasenv, substitution *)
  int * NCic.conjecture ->                       (* sequent *)
-  Gdome.document                                (* Math ML *)
+  Gdome.document *                              (* Math ML *)
+  (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *)
 
 val mml_of_cic_object:
   Cic.obj ->                                  (* object *)
@@ -60,7 +61,10 @@ val mml_of_cic_object:
        (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
        (Cic.id, Cic2acic.anntypes) Hashtbl.t))  (* ids_to_inner_types *)
 
-val nmml_of_cic_object: NCic.obj -> Gdome.document
+val nmml_of_cic_object:
+ NCic.obj -> Gdome.document *
+  (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *)
+
 
 val txt_of_cic_term: 
   map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->