X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.mli;h=b0d7243796a06c4582b91415fb0a8b3e9babffa5;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=87b2e8e4b86e372029749be7c3622cf65959ef8f;hpb=433e66b381d1b89e48c05d517494fc300fd0abb5;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli
index 87b2e8e4b..b0d724379 100644
--- a/matita/components/ng_tactics/nnAuto.mli
+++ b/matita/components/ng_tactics/nnAuto.mli
@@ -9,29 +9,27 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+type auto_params = NTacStatus.tactic_term list option * (string * string) list
+
 val is_a_fact_obj: 
   #NTacStatus.pstatus -> NUri.uri -> bool
 
-val fast_eq_check_tac:
-  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
-   's NTacStatus.tactic
+val fast_eq_check_tac: params:auto_params -> 's NTacStatus.tactic
 
-val paramod_tac:
-  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
-   's NTacStatus.tactic
+val paramod_tac: params:auto_params -> 's NTacStatus.tactic
 
-val demod_tac:
-  params:(NTacStatus.tactic_term list option* (string * string) list) -> 
-   's NTacStatus.tactic
+val demod_tac: params:auto_params -> 's NTacStatus.tactic
 
 val smart_apply_tac: 
   NTacStatus.tactic_term -> 's NTacStatus.tactic
 
 val auto_tac:
-  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
+  params:auto_params ->
    ?trace_ref:NotationPt.term list ref -> 
    's NTacStatus.tactic
 
+val auto_lowtac: params:auto_params -> NTacStatus.lowtac_status -> int -> NTacStatus.lowtac_status
+
 val keys_of_type: 
   (#NTacStatus.pstatus as 'a) ->
   NTacStatus.cic_term -> 'a * NTacStatus.cic_term list