From c9fd02dc38c607c53b682e35bca553d54c7fe648 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 15 Oct 2001 13:04:56 +0000
Subject: Export hide_ident_or_numarg_tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2119 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.mli | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7205303b2..75235b657 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. *)
 
-- 
cgit v1.2.3