Changes to declarative tactics, implementation of equality chain

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

diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli
index fd5916c8dbf69f1add0deb3cf9beaa53bd8245e5..250b26991625442e6d2d46559541ac20d3c4c42a 100644 (file)
--- a/matita/components/ng_tactics/nTactics.mli
+++ b/matita/components/ng_tactics/nTactics.mli
@@ -92,3 +92,4 @@ val inversion_tac:
      's NTacStatus.tactic
 
 val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
+val first_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic