]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_tactics/nnAuto.mli
Trying to be faster.
[helm.git] / helm / software / components / ng_tactics / nnAuto.mli
index 7a381cbdc3305b463503e67131ba557b1a913bfb..e08d0456d2468988c5c23665be1d51ee0f8bbecc 100644 (file)
@@ -16,6 +16,9 @@ val fast_eq_check_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
+val smart_apply_tac: 
+  NTacStatus.tactic_term -> 's NTacStatus.tactic
+
 val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic