X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.mli;h=dbd0343ff600d4bdd3e09e62963c340e5adcacdb;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=1297be57f26dd55ed688ebc11745317c70daea5b;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git

diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli
index 1297be57f..dbd0343ff 100644
--- a/helm/software/matita/applyTransformation.mli
+++ b/helm/software/matita/applyTransformation.mli
@@ -45,6 +45,7 @@ val mml_of_cic_sequent:
      (Cic.id, Cic2acic.sort_kind) Hashtbl.t))   (* ids_to_inner_sorts *)
 
 val nmml_of_cic_sequent:
+ #NCicCoercion.status ->
  NCic.metasenv -> NCic.substitution ->          (* metasenv, substitution *)
  int * NCic.conjecture ->                       (* sequent *)
   Gdome.document                                (* Math ML *)
@@ -60,6 +61,8 @@ 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: #NCicCoercion.status -> NCic.obj -> Gdome.document
+
 val txt_of_cic_term: 
   map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
    string