tactic cases works! delift clears tags

[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 1feac415baec232ebd9fdeeeb6fbc031156de2fd..6c7d698239f96fa5ac7efba9e11f8053254cc214 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -33,6 +33,7 @@ type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 type cic_term 
 val ctx_of : cic_term -> NCic.context
+val term_of_cic_term : cic_term -> NCic.context -> NCic.term
 
 val mk_cic_term : NCic.context -> NCic.term -> cic_term
 type ast_term = string * int * CicNotationPt.term
@@ -59,8 +60,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