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, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e3aa5d7921..00f15a62a5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -173,6 +173,8 @@ Tactics
 - The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
 - New tactic "enough", symmetric to "assert", but with subgoals
   swapped, as a more friendly replacement of "cut".
+- In destruct/induction, experimental modifier "!" prefixing the
+  hypothesis name to tell not erasing the hypothesis.
 
 Program