Experimentally adding an option for automatically erasing an

hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).

Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).

1 files changed, 17 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 28d854eaa..a3953bb96 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1573,6 +1573,14 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
+\item{\tt destruct !{\ident}}
+
+  This is a case when the destructed term is an hypothesis of the
+  context. The ``!'' modifier tells to keep the hypothesis in the
+  context after destruction.
+
+  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
+
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1750,6 +1758,15 @@ induction n.
   einduction}.  It combines the effects of the {\tt with}, {\tt as},
   {\tt eqn:}, {\tt using}, and {\tt in} clauses.
 
+\item{\tt induction !{\ident}}
+
+  This is a case when the term on which to apply induction is an
+  hypothesis of the context. The ``!'' modifier tells to keep the
+  hypothesis in the context after induction.
+
+  This applies also to the other form of {\tt induction} and {\tt
+    einduction}.
+
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the