Added an implicit parameter to branch_tac to allow branching on a

[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 efb4e843c99a2e91da86a04144f657c666370c55..74bbcbcb4214a3565506a04d1dc81695bf746970 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -12,7 +12,7 @@
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
 val dot_tac: 's NTacStatus.tactic
-val branch_tac: 's NTacStatus.tactic
+val branch_tac: ?force:bool -> 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
 val pos_tac: int list -> 's NTacStatus.tactic
 val case_tac: string -> 's NTacStatus.tactic