X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=0653223af39fcae890932ec36878835485a572c2;hb=9e30dacbcdb10a58d6cf8f3995d1a195f2b31f4b;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..0653223af 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 
@@ -59,7 +60,6 @@ val refine:
 val apply_subst:
   lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
-
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: 
    lowtac_status -> ?name:string -> NCic.context ->