Cosmetic.

[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 3963f2500943ad1c6a793b8202398025b6e0af87..0653223af39fcae890932ec36878835485a572c2 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -37,9 +37,8 @@ val term_of_cic_term :
       lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term
 
 val mk_cic_term : NCic.context -> NCic.term -> cic_term
-type ast_term = string * int * CicNotationPt.term
 val disambiguate:
-  lowtac_status -> ast_term -> cic_term option -> NCic.context -> 
+  lowtac_status -> tactic_term -> cic_term option -> NCic.context -> 
     lowtac_status * cic_term (* * cic_term XXX *)
 
 val analyse_indty: 
@@ -47,6 +46,7 @@ val analyse_indty:
     lowtac_status * 
       (NReference.reference * int * NCic.term list * NCic.term list)
 
+val ppterm: lowtac_status -> cic_term -> string
 val whd: 
       lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
         lowtac_status * cic_term 
@@ -57,6 +57,8 @@ val unify:
 val refine: 
   lowtac_status -> NCic.context -> cic_term -> cic_term option -> 
     lowtac_status * cic_term * cic_term (* status, term, type *)
+val apply_subst:
+  lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: 
@@ -69,7 +71,7 @@ val select_term:
   lowtac_status -> 
   found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
   postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
-  cic_term -> ast_term option * NCic.term ->
+  cic_term -> tactic_term option * NCic.term ->
     lowtac_status * cic_term
 
 val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term