Added ppterm.

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 55448ae2db03615416aec06118be58bacb492a58..f8ee5f1e5e929ab197773adaf6c8be5a567c0f3e 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -99,6 +99,12 @@ let term_of_cic_term s t c =
   s, t
 ;;
 
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let _,context,t = t in
+  NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
 let disambiguate status t ty context =
  let status, expty = 
    match ty with 

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index c0f0ca4db019d2d25963612581daec13d99a4ffb..74b5366db396b5dee570fc213415a35f1764cca8 100644 (file)
--- 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