X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.mli;h=d77d32085813510d178e5848b8ff9c99bf001996;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=2376a773ad3ad7db387e74e98bbe6d8b19ce80c1;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli
index 2376a773a..d77d32085 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) -> 
-   ?trace_ref:CicNotationPt.term list ref -> 
+  params:auto_params ->
+   ?trace_ref:NotationPt.term list ref -> 
    's NTacStatus.tactic
 
+val auto_lowtac: params:auto_params -> #NTacStatus.pstatus -> int -> 's NTacStatus.tactic
+
 val keys_of_type: 
   (#NTacStatus.pstatus as 'a) ->
   NTacStatus.cic_term -> 'a * NTacStatus.cic_term list