diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-15 13:04:56 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-15 13:04:56 +0000 |
commit | c9fd02dc38c607c53b682e35bca553d54c7fe648 (patch) | |
tree | e910bae783b201ea1cfdac852f25766f73ab6cb0 | |
parent | c6a4c593148f72aa5de5294c82b4dcd42be078c8 (diff) |
Export hide_ident_or_numarg_tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2119 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/tactics.mli | 7 |
1 files changed, 7 insertions, 0 deletions
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. *) |