apply_subst_context on statuses

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

diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index 13a519d70903c5b4eef34c3b4bdca5d08efd1fb1..8f56541e3d95732e3cbd732e1e4cd556b3538623 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -13,21 +13,25 @@ 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 * (string * string) list) -> 
+  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) -> 
    's NTacStatus.tactic
 
+val keys_of_type: 
+  (#NTacStatus.pstatus as 'a) ->
+  NTacStatus.cic_term -> 'a * NTacStatus.cic_term list
+