X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=74b5366db396b5dee570fc213415a35f1764cca8;hb=6bd0d331d096d862754b42f9a7fb8af1b823685d;hp=c0f0ca4db019d2d25963612581daec13d99a4ffb;hpb=8d7287519cc51145fcac0ee603ba136dc749857d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index c0f0ca4db..74b5366db 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -46,6 +46,7 @@ val analyse_indty:
     lowtac_status * 
       (NReference.reference * int * NCic.term list * NCic.term list)
 
+val ppterm: lowtac_status -> cic_term -> string
 val whd: 
       lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
         lowtac_status * cic_term