First tests for paramodulation (pretty printer, unification)

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

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 3e13035eb792d4188a976d88137f9fe0989a2b36..142300cc0bb91d30d74ef1381adb53fe0678f02f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -51,3 +51,6 @@ val letin_tac:
 val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   NTacStatus.tactic
+
+val auto_tac:
+  params:'a -> NTacStatus.tactic