Release 0.5.9.

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

diff --git a/helm/software/components/ng_tactics/nDestructTac.mli b/helm/software/components/ng_tactics/nDestructTac.mli
index 714638d24f56dcba221c3767f4e88474a289d9fa..a51886511e3d19da77437745c2ffda2d838900f7 100644 (file)
--- a/helm/software/components/ng_tactics/nDestructTac.mli
+++ b/helm/software/components/ng_tactics/nDestructTac.mli
@@ -11,5 +11,4 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val destruct_tac : string list option -> string list -> 's NTacStatus.tactic
-
+val destruct_tac : 's NTacStatus.tactic