Fixing naming scheme for composite coercions.

[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 6e4cc79ddb90405c20b5473f35f4d7a8f2f887f5..5616794573ed830c42ab14913de5a61501f90d78 100644 (file)
--- 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 *)