Merge remote-tracking branch 'origin/ld-0.99.3'

[helm.git] / matita / components / ng_tactics / nnAuto.mli

diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli
index 2376a773ad3ad7db387e74e98bbe6d8b19ce80c1..d77d32085813510d178e5848b8ff9c99bf001996 100644 (file)
--- 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