X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.mli;h=f41f0a7a1e27ad38e1fcf5240c954c0823e1f77d;hb=a17430d258e886b5164fca3d65ee7da7c40e6a36;hp=1297be57f26dd55ed688ebc11745317c70daea5b;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 1297be57f..f41f0a7a1 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -60,6 +60,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: NCic.obj -> Gdome.document + val txt_of_cic_term: map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> string