Cosmetic.

[helm.git] / helm / software / components / ng_tactics / nTacStatus.mli

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 81436f53d63c48f5f534c8618efe8a796dbd6e68..0653223af39fcae890932ec36878835485a572c2 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 
@@ -56,6 +57,8 @@ val unify:
 val refine: 
   lowtac_status -> NCic.context -> cic_term -> cic_term option -> 
     lowtac_status * cic_term * cic_term (* status, term, type *)
+val apply_subst:
+  lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: