new tactic constructor: @[n]

[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 c81b1dd0bab0ae8e202d1dab47a1f9e5261df5ff..b282b04cace74fee82423b151dffa320b4eef57a 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -59,3 +59,5 @@ val assert_tac:
 val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
+
+val constructor_tac : ?num:int -> 's NTacStatus.tactic