X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=5616794573ed830c42ab14913de5a61501f90d78;hb=4c4228417fc38e71bce647174d175561db2afb01;hp=6e4cc79ddb90405c20b5473f35f4d7a8f2f887f5;hpb=1e5771907d96b66df32beb557bf775add3fb8dd7;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 6e4cc79dd..561679457 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -63,6 +63,8 @@ val refine:
   'status * cic_term * cic_term (* status, term, type *)
 val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
+val apply_subst_context :
+  #pstatus -> fix_projections:bool -> NCic.context -> NCic.context
 val fix_sorts: #pstatus as 'status -> cic_term -> 'status * cic_term
 val saturate :
  #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
@@ -88,8 +90,6 @@ val mk_in_scope: #pstatus as 'status -> cic_term -> 'status * cic_term
 val mk_out_scope:
  int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term
 
-val pp_status: #pstatus -> unit
-
 class type ['stack] g_status =
  object
   inherit g_pstatus
@@ -111,6 +111,8 @@ type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
 
 class type tac_status = [Continuationals.Stack.t] status
 
+val pp_tac_status: #tac_status -> unit
+
 type 'status tactic = #tac_status as 'status -> 'status
 
 (* indexing facilities over cic_term based on inverse De Bruijn indexes *)