unification:

[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 4ca302890808c584c32bfcef9cc810700ca7396e..ce3fd33b03c39da2b2a57f11d7da65c3e6e1a7b3 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -59,10 +59,10 @@ val mk_meta:
      lowtac_status * cic_term
 val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
 
-val in_scope_tag: string
-val out_scope_tag: string
 val select_term:
   lowtac_status -> cic_term -> ast_term option * NCic.term ->
     lowtac_status * cic_term
 
+val pp_tac_status: tac_status -> unit
+
 (* end *)