Moved compare in a different file.

[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 e08d0456d2468988c5c23665be1d51ee0f8bbecc..13a519d70903c5b4eef34c3b4bdca5d08efd1fb1 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -16,6 +16,14 @@ val fast_eq_check_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
+val paramod_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
+
+val demod_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
+
 val smart_apply_tac: 
   NTacStatus.tactic_term -> 's NTacStatus.tactic
 
@@ -23,4 +31,3 @@ val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
-val debug : bool ref