Export hide_ident_or_numarg_tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2119 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7205303b23..75235b6577 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -90,6 +90,13 @@ val intros_clearing      : bool list -> tactic
    hypothesis is already in context and directly apply [tac] *)
 val tactic_try_intros_until : (identifier,tactic_arg) parse_combinator
 
+(* Assuming a tactic [tac] depending on an hypothesis identifier,
+   [hide_ident_or_numarg_tactic str tac] registers a tactic which
+   compose [tac] with "Intros Until" and returns a tactic which
+   behaves as [tac] (without implicit "Intros until") but hiding the
+   implementation under the name [str] *)
+
+val hide_ident_or_numarg_tactic : identifier hide_combinator
 
 (*s Exact tactics. *)