X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=ce3fd33b03c39da2b2a57f11d7da65c3e6e1a7b3;hb=86ff79af764c2a434fdf38ea344ab722811981c8;hp=1feac415baec232ebd9fdeeeb6fbc031156de2fd;hpb=718d9bcfb53dd76a5c0622aff9fed69a68769324;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 1feac415b..ce3fd33b0 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -59,8 +59,6 @@ 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