X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=307154127269847e22ce56570ae6f7f5199027f3;hb=c091ca7a030a85a529543de98e45c54284028b63;hp=6c7d698239f96fa5ac7efba9e11f8053254cc214;hpb=4b6193be548c96964beee706b75a06e269eed88d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 6c7d69823..307154127 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -16,7 +16,7 @@ val fail: string lazy_t -> 'a
 
 type lowtac_status = {
         pstatus : NCic.obj;
-        lstatus : LexiconEngine.status
+        estatus : NEstatus.status;
 }
 
 type lowtactic = lowtac_status -> int -> lowtac_status 
@@ -33,25 +33,35 @@ 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 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: 
   lowtac_status -> cic_term -> 
-    NReference.reference * int * NCic.term list * NCic.term list
+    lowtac_status * 
+      (NReference.reference * int * NCic.term list * NCic.term list)
 
-val whd: lowtac_status -> ?delta:int -> NCic.context -> cic_term -> cic_term 
-val typeof: lowtac_status -> NCic.context -> cic_term -> cic_term
+val ppterm: lowtac_status -> cic_term -> string
+val whd: 
+      lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
+        lowtac_status * cic_term 
+val normalize: 
+      lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
+        lowtac_status * cic_term 
+val typeof: 
+      lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 val unify: 
   lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
 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: 
@@ -61,9 +71,15 @@ val mk_meta:
 val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
 
 val select_term:
-  lowtac_status -> cic_term -> ast_term option * NCic.term ->
+  lowtac_status -> 
+  found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
+  postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
+  cic_term -> tactic_term option * NCic.term ->
     lowtac_status * cic_term
 
+val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term
+val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term
+
 val pp_tac_status: tac_status -> unit
 
 (* end *)