X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.mli;h=2376a773ad3ad7db387e74e98bbe6d8b19ce80c1;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=7d59d395d6e8cd2565725bf61a6c17f22dd33467;hpb=36fae35c9cbbf8df389a3f34cd1ee6921b6029fd;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index 7d59d395d..2376a773a 100644
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -13,17 +13,26 @@ val is_a_fact_obj:
   #NTacStatus.pstatus -> NUri.uri -> bool
 
 val fast_eq_check_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
    's NTacStatus.tactic
 
 val paramod_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
+   's NTacStatus.tactic
+
+val demod_tac:
+  params:(NTacStatus.tactic_term list option* (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) -> 
+  params:(NTacStatus.tactic_term list option * (string * string) list) -> 
+   ?trace_ref:CicNotationPt.term list ref -> 
    's NTacStatus.tactic
 
+val keys_of_type: 
+  (#NTacStatus.pstatus as 'a) ->
+  NTacStatus.cic_term -> 'a * NTacStatus.cic_term list
+